Function vstd::set_lib::lemma_set_union_finite_implies_sets_finite

source · 
pub proof fn lemma_set_union_finite_implies_sets_finite<A>(s1: Set<A>, s2: Set<A>)
Expand description
requires
s1.union(s2).finite(),
ensures
s1.finite(),
s2.finite(),