Function vstd::set::axiom_set_choose_len

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

A finite set s contains the element s.choose() if it has length greater than 0.