Function vstd::set::axiom_set_contains_len

source · 
pub broadcast proof fn axiom_set_contains_len<A>(s: Set<A>, a: A)
Expand description
requires
s.finite(),
#[trigger] s.contains(a),
ensures
#[trigger] s.len() != 0,

If a finite set s contains any element, it has length greater than 0.