Function vstd::set::axiom_set_remove_finite
source · pub broadcast proof fn axiom_set_remove_finite<A>(s: Set<A>, a: A)Expand description
requires
s.finite(),#[trigger] s.remove(a).finite(),The result of removing an element a from a finite set s is also finite.