pub broadcast proof fn lemma_iset_empty_len<A>()Expand description
ensures
#[trigger] ISet::<A>::empty().len() == 0,The empty set has length 0.
pub broadcast proof fn lemma_iset_empty_len<A>()#[trigger] ISet::<A>::empty().len() == 0,The empty set has length 0.