Function vstd::set::axiom_set_remove_different

source ·

pub broadcast proof fn axiom_set_remove_different<A>(s: Set<A>, a1: A, a2: A)

Expand description

requires

a1 != a2,

ensures

#[trigger] s.remove(a2).contains(a1) == s.contains(a1),

If a1 does not equal a2, then the result of removing element a2 from set s must contain a1 if and only if the set contained a1 before the removal of a2.