pub broadcast proof fn lemma_iset_insert_finite<A>(s: ISet<A>, a: A)Expand description
requires
s.finite(),#[trigger] s.insert(a).finite(),The result of inserting an element a into a finite set s is also finite.