proposition: Theorem inject_monoR (beta gamma : T1) : T1.nf beta -> T1.nf gamma -> inject beta < inject gamma -> (beta t1< gamma)%t1.
proof: Proof. intros H H0 H1; destruct (T1.lt_eq_lt_dec beta gamma) as [[H2 | H2] | H2]. - now split. - subst ; case (lt_irrefl H1). - destruct (@lt_irrefl (inject beta)). eapply lt_trans with (inject gamma); auto. now apply inject_mono. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)