proposition: Lemma AP_phi0 (alpha : Ord) : In AP (phi0 alpha).
proof: Proof. pattern phi0; apply phi0_elim. destruct 1 as [H H0 H1 H2]; apply H0;auto; split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)