Function vstd::set::axiom_set_insert_finite

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

The result of inserting an element a into a finite set s is also finite.