Function vstd::multiset::lemma_update_same
source · pub proof fn lemma_update_same<V>(m: Multiset<V>, v: V, mult: nat)Expand description
ensures
m.update(v, mult).count(v) == mult,The multiset resulting from updating a value v in a multiset m to multiplicity mult will
have a count of mult for v.