proposition: Lemma of_beta' : ordering_function _f _A (proper_segment_of B beta).
proof: Proof. pattern _f; unfold _f; apply epsilon_spec; destruct (H_B beta_B) as [x [H1 H2]]. case H1; intros x0 H; exists x0;auto. unfold _A; apply iota_ind. - exists x; split; auto. - intros a H0; destruct H0; replace a with x; auto. Qed.
imports: ZornsLemma(CountableTypes)