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(),#[trigger] s.contains(s.choose()),An infinite set s contains the element s.choose().