vstd::multiset

Function lemma_insert_len

Source
pub broadcast proof fn lemma_insert_len<V>(m: Multiset<V>, x: V)
Expand description
ensures
#[trigger] m.insert(x).len() == m.len() + 1,

Inserting an element x into a multiset m will increase the length of m by 1.