pub broadcast proof fn lemma_iset_ext_equal<A>(s1: ISet<A>, s2: ISet<A>)Expand description
ensures
#[trigger] (s1 =~= s2) <==> (forall |a: A| s1.contains(a) == s2.contains(a)),ISets s1 and s2 are equal if and only if they contain all of the same elements.