Function vstd::set_lib::axiom_is_empty

source · 
pub broadcast proof fn axiom_is_empty<A>(s: Set<A>)
Expand description
requires
s.finite(),
!(#[trigger] s.is_empty()),
ensures
exists |a: A| s.contains(a),