Function vstd::seq_lib::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)