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