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,#[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.