pub broadcast proof fn lemma_iset_insert_len<A>(s: ISet<A>, a: A)Expand description
requires
s.finite(),#[trigger] s.insert(a).len() == s.len() + (if s.contains(a) { 0int } else { 1 }),The result of inserting an element a into a finite set s has length
s.len() + 1 if a is not already in s and length s.len() otherwise.