pub broadcast proof fn lemma_iset_remove_same<A>(s: ISet<A>, a: A)
!(#[trigger] s.remove(a).contains(a)),
The result of removing element a from set s must not contain a.
a
s