proposition: Lemma phi0_inj (alpha beta : Ord) : phi0 alpha = phi0 beta -> alpha = beta.
proof: Proof. intros; apply le_antisym; apply phi0_mono_R_weak;auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)