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.