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.