Function vstd::set_lib::lemma_set_insert_finite_iff

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

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