proposition: Lemma phi_le : forall alpha beta alpha' beta', nf beta -> phi alpha beta = [alpha', beta'] -> alpha t2<= alpha'.
proof: Proof. intros a b a' b' Hb;case (phi_cases a Hb). - destruct 1. + case (phi_fix _ e); intros x (beta2,(H,H0)). rewrite e, H; injection 1; intros; subst x; right;auto with T2. + rewrite e;injection 1;left;auto with T2. - intros (b0,(H1,(H2,H3))). rewrite H2; injection 1;left;auto with T2. 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)