proposition: Lemma phi0_lt_epsilon0 (alpha : Ord) : alpha < epsilon0 -> phi0 alpha < epsilon0.
proof: Proof. intro; rewrite <- epsilon0_fxp; now apply phi0_mono. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)