pub broadcast proof fn lemma_iset_union_finite_iff<A>(s1: ISet<A>, s2: ISet<A>)Expand description
ensures
#[trigger] s1.union(s2).finite() <==> s1.finite() && s2.finite(),The union of two sets is finite iff both sets are finite.