proposition: Lemma lt_epsilon0_okR: forall alpha, nf alpha -> alpha t2< epsilon0 -> lt_epsilon0 alpha.
proof: Proof. induction alpha. - constructor. - intros; inversion H0. + rewrite (lt_one_inv H3). right. * apply IHalpha2. inversion H;auto with T2. compute;auto with T2. * apply IHalpha3. inversion H;auto with T2. compute;auto with T2. apply lt_trans with (gcons alpha1 alpha2 n alpha3). apply lt_tail. auto with T2. auto with T2. + inversion H2. + inversion H10. + inversion H2. + inversion H2. 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)