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.