Function vstd::set::axiom_set_insert_different

source · 
pub broadcast proof fn axiom_set_insert_different<A>(s: Set<A>, a1: A, a2: A)
Expand description
requires
a1 != a2,
ensures
#[trigger] s.insert(a2).contains(a1) == s.contains(a1),

If a1 does not equal a2, then the result of inserting element a2 into set s must contain a1 if and only if the set contained a1 before the insertion of a2.