pub broadcast proof fn lemma_iset_union_finite<A>(s1: ISet<A>, s2: ISet<A>)Expand description
requires
s1.finite(),s2.finite(),#[trigger] s1.union(s2).finite(),The union of two finite sets is finite.