pub broadcast proof fn to_multiset_insert<A>(s: Seq<A>, i: int, a: A)Expand description
requires
0 <= i <= s.len(),s.insert(i, a).to_multiset() == s.to_multiset().insert(a),