pub broadcast proof fn lemma_iset_difference<A>(s1: ISet<A>, s2: ISet<A>, a: A)Expand description
ensures
#[trigger] s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)),The set difference between s1 and s2 contains element a if and only if
s1 contains a and s2 does not contain a.