proposition: Theorem normal_phi0 : normal phi0 AP.
proof: Proof. apply TH_13_6R with ordinal. - unfold _phi0; rewrite <- AP_o_segment; apply ord_ok. - apply AP_closed. - apply AP_unbounded. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)