Function vstd::set::axiom_set_empty

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

The empty set contains no elements