Function vstd::multiset::lemma_insert_other_elements_unchanged

source · 
pub proof fn lemma_insert_other_elements_unchanged<V>(m: Multiset<V>, x: V, y: V)
Expand description
ensures
x != y ==> m.count(y) == m.insert(x).count(y),

Inserting an element x into a multiset m will not change the count of any other element y in m.