Function lemma_iset_union_finite_implies_sets_finite

pub proof fn lemma_iset_union_finite_implies_sets_finite<A>(s1: ISet<A>, s2: ISet<A>)

Expand description

requires

s1.union(s2).finite(),

ensures

s1.finite(),

s2.finite(),

If the union of two ISets is finite, then each of those ISets is also finite.

lemma_iset_union_finite_implies_sets_finite