Function lemma_iset_ext_equal_deep Copy item path

pub broadcast proof fn lemma_iset_ext_equal_deep<A>(s1: ISet<A>, s2: ISet<A>)

#[trigger] (s1 =~~= s2) <==> (s1 =~= s2),