Function vstd::set::axiom_set_remove_insert

source · 
pub broadcast proof fn axiom_set_remove_insert<A>(s: Set<A>, a: A)
Expand description
requires
s.contains(a),
ensures
(#[trigger] s.remove(a)).insert(a) == s,

Removing an element a from a set s and then inserting a back into the setis equivalent to the original sets`.