Function vstd::set_lib::lemma_set_difference2

pub proof fn lemma_set_difference2<A>(s1: Set<A>, s2: Set<A>, a: A)

Expand description

ensures

s2.contains(a) ==> !s1.difference(s2).contains(a),

If set s2 contains element a, then the set difference of s1 and s2 does not contain a.