pub broadcast proof fn lemma_set_insert_finite_iff<A>(s: Set<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.