pub proof fn lemma_len_difference<A>(s1: Set<A>, s2: Set<A>)Expand description
ensures
s1.difference(s2).len() <= s1.len(),The size of the difference of finite set s1 and set s2 is less than or equal to the size of s1.