pub broadcast proof fn lemma_iset_empty_finite<A>()Expand description
ensures
#[trigger] ISet::<A>::empty().finite(),The empty set is finite.
pub broadcast proof fn lemma_iset_empty_finite<A>()#[trigger] ISet::<A>::empty().finite(),The empty set is finite.