Function vstd::set::axiom_set_choose_finite

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

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