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,#[trigger] s.contains(s.choose()),A finite set s contains the element s.choose() if it has length greater than 0.