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