pub broadcast proof fn lemma_iset_empty_equivalency_len<A>(s: ISet<A>)Expand description
requires
s.finite(),(s.len() == 0 <==> s == ISet::<A>::empty())
&& (s.len() != 0 ==> exists |x: A| s.contains(x)),ISet s has length 0 if and only if it is equal to the empty set. If s has length greater than 0,
Then there must exist an element x such that s contains x.