Function vstd::set_lib::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.