proposition: Theorem inject_lt_epsilon0_ex (alpha : Ord) (H : alpha < epsilon0) : exists t: T1, nf t /\ inject t = alpha.
proof: Proof. destruct (cnf_exists alpha) as [l Hl]. destruct (inject_lt_epsilon0_ex_cnf alpha H l Hl) as [t [H1 H2]]. exists t; split ; [trivial | ]. destruct Hl; congruence. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)