proposition: Lemma phi0_elim : forall P : (Ord->Ord)->Prop, (forall f: Ord->Ord, ordering_function f ordinal AP -> P f) -> P phi0.
proof: Proof. intros P H; apply H, phi0_ordering. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)