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.