proposition: Lemma g_lemma : forall beta, In B beta -> ordering_function (_f beta) (members (g beta)) (proper_segment_of B beta).
proof: Proof. intros beta H; rewrite <- g_def. - now apply of_beta'. - assumption. Qed.
imports: ZornsLemma(CountableTypes)