proposition: Theorem inject_lt_epsilon0_ex_unique (alpha : Ord) (H : alpha < epsilon0) : exists! t: T1, nf t /\ inject t = alpha.
proof: Proof. destruct (inject_lt_epsilon0_ex alpha H ) as [t [H0 H1]]. exists t; split. - now split. - intros t' [H2 H3]. rewrite <- H3 in H1; now apply inject_injective. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)