Function vstd::multiset::lemma_insert_len
source · pub proof fn lemma_insert_len<V>(m: Multiset<V>, x: V)Expand description
ensures
m.insert(x).len() == m.len() + 1,Inserting an element x into a multiset m will increase the length of m by 1.