Function vstd::set_lib::lemma_len_subset

source · 
pub proof fn lemma_len_subset<A>(s1: Set<A>, s2: Set<A>)
Expand description
requires
s2.finite(),
s1.subset_of(s2),
ensures
s1.len() <= s2.len(),
s1.finite(),

If s1 is a subset of finite set s2, then the size of s1 is less than or equal to the size of s2 and s1 must be finite.