vstd::seq_lib

Function to_multiset_build

Source
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)