Function vstd::set_lib::lemma_len_intersect

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

The size of the intersection of finite set s1 and set s2 is less than or equal to the size of s1.