Function vstd::set::axiom_set_remove_len
source · pub broadcast proof fn axiom_set_remove_len<A>(s: Set<A>, a: A)Expand description
requires
s.finite(),s.len() == #[trigger] s.remove(a).len() + (if s.contains(a) { 1int } else { 0 }),The result of removing an element a from a finite set s has length
s.len() - 1 if a is in s and length s.len() otherwise.