pub broadcast proof fn lemma_iset_insert_same<A>(s: ISet<A>, a: A)
#[trigger] s.insert(a).contains(a),
The result of inserting element a into set s must contains a.
a
s