proposition: Lemma plus_lt_phi0 (ksi alpha: Ord): ksi < phi0 alpha -> ksi + phi0 alpha = phi0 alpha.
proof: Proof. pattern (phi0 alpha); apply phi0_elim; intros f Hf; assert (H: AP (f alpha)). { destruct Hf as [H0 H1 H2 H3]. apply H1 ; split. } destruct H; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)