vstd::set_lib

Function lemma_set_subset_finite

Source 
pub broadcast proof fn lemma_set_subset_finite<A>(s: Set<A>, sub: Set<A>)
Expand description
requires
s.finite(),
sub.subset_of(s),
ensures
sub.finite(),

A subset of a finite set s is finite.