Function lemma_set_new_from_iset

pub broadcast proof fn lemma_set_new_from_iset<A>(s: ISet<A>)

Expand description

requires

s.finite(),

ensures

Set::<A>::new_from_iset(s) is Some,

Set::<A>::new_from_iset(s).unwrap().to_iset() == s,

If an iset s is finite, then Set::new_from_iset(s) has the same contents as s.

lemma_set_new_from_iset