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.