proposition: Lemma AP_to_phi0 (alpha : Ord) : AP alpha -> exists beta, alpha = phi0 beta.
proof: Proof. intro H; pattern phi0;apply phi0_elim. destruct 1 as [H0 H1 H2 H3]. case (H2 _ H); intros x [_ H4]; exists x; now rewrite H4. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)