Function vstd::set::axiom_set_complement

source · 
pub broadcast proof fn axiom_set_complement<A>(s: Set<A>, a: A)
Expand description
ensures
#[trigger] s.complement().contains(a) == !s.contains(a),

The complement of set s contains element a if and only if s does not contain a.