proposition: Theorem inject_lt_epsilon0 (alpha : T1): inject alpha < epsilon0.
proof: Proof. assert (Ap := epsilon0_AP); induction alpha; simpl. - rewrite <- epsilon0_fxp; apply phi0_positive. - apply AP_plus_closed; auto. apply AP_mult_Sn_closed; auto. now apply phi0_lt_epsilon0. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)