Function vstd::set::axiom_set_insert_same

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

The result of inserting element a into set s must contains a.