Function vstd::multiset::lemma_insert_increases_count_by_1

source · 
pub proof fn lemma_insert_increases_count_by_1<V>(m: Multiset<V>, x: V)
Expand description
ensures
m.insert(x).count(x) == m.count(x) + 1,

Inserting an element x into multiset m will increase the count of x in m by 1.