proposition: Lemma inj_monoR : forall c c', lt (T1_inj c) (T1_inj c') -> (c < c')%ca.
proof: Proof. intros. case (EPSILON0.trichotomy_inf c c'). destruct 1. auto with T2. subst c'. case (lt_irr H). intro. generalize (inj_mono l). intro. case (lt_irr (alpha:=T1_inj c)). eapply transitivity;eauto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo