pub broadcast proof fn to_multiset_build<A>(s: Seq<A>, a: A)Expand description
ensures
s.push(a).to_multiset() =~= s.to_multiset().insert(a),push(a) o to_multiset = to_multiset o insert(a)