pub broadcast proof fn lemma_iset_empty<A>(a: A)Expand description
ensures
!(#[trigger] ISet::empty().contains(a)),The empty set contains no elements
pub broadcast proof fn lemma_iset_empty<A>(a: A)!(#[trigger] ISet::empty().contains(a)),The empty set contains no elements