Function vstd::set::axiom_set_remove_same
source · pub broadcast proof fn axiom_set_remove_same<A>(s: Set<A>, a: A)Expand description
ensures
!(#[trigger] s.remove(a).contains(a)),The result of removing element a from set s must not contain a.