pub broadcast proof fn lemma_iset_complement<A>(s: ISet<A>, a: A)Expand description
ensures
#[trigger] s.complement().contains(a) == !s.contains(a),The complement of set s contains element a if and only if s does not contain a.