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