proposition: Theorem inject_mono (beta gamma : T1) : T1.lt beta gamma -> T1.nf beta -> T1.nf gamma -> inject beta < inject gamma.
proof: Proof. intros H H0 H1; apply inject_mono_0 with (T1.succ gamma);auto. - apply T1.succ_nf;auto. - apply T1.lt_succ;auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)