vstd::set

Function axiom_set_choose_infinite

Source 
pub broadcast proof fn axiom_set_choose_infinite<A>(s: Set<A>)
Expand description
requires
!s.finite(),
ensures
#[trigger] s.contains(s.choose()),

An infinite set s contains the element s.choose().