proposition: Lemma T1_to_T2_mono : forall alpha beta, T1.lt alpha beta -> T1_to_T2 alpha t2< T1_to_T2 beta.
proof: Proof. induction alpha. + destruct beta. * intro H; compute in H; discriminate. * cbn; constructor. + destruct beta. * intro H; compute in H; discriminate. * intro H; destruct (lt_inv H). -- constructor 3; now apply IHalpha1. -- decompose [or and] H0; clear H0; subst alpha1. ++ now constructor 6. ++ subst n; constructor 7; now apply IHalpha2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)