Function vstd::set_lib::lemma_len_union_ind

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

The size of a union of two sets is greater than or equal to the size of both individual sets.