pub broadcast proof fn lemma_iset_choose_infinite<A>(s: ISet<A>)Expand description
requires
!s.finite(),#[trigger] s.contains(s.choose()),An infinite set s contains the element s.choose().