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