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.