Function vstd::set::axiom_set_ext_equal

pub broadcast proof fn axiom_set_ext_equal<A>(s1: Set<A>, s2: Set<A>)

Expand description

ensures

#[trigger] (s1 =~= s2) <==> (forall |a: A| s1.contains(a) == s2.contains(a)),

Sets s1 and s2 are equal if and only if they contain all of the same elements.

Function vstd::set::axiom_set_ext_equalCopy item path