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