Skip to main content

lemma_to_iset_finite

vstd::set

Function lemma_to_iset_finite 

Source 
pub broadcast proof fn lemma_to_iset_finite<A>(s: Set<A>)
Expand description
ensures
#[trigger] s.to_iset().finite(),

Converting a Set to an ISet produces a finite result.