Skip to main content

lemma_to_iset_len

vstd::set

Function lemma_to_iset_len 

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

Converting a Set to an ISet produces a result with the same length.