proposition: Lemma phi_le_ge : forall alpha beta, nf alpha -> nf beta -> {alpha':T2 & {beta':T2 | phi alpha beta = [alpha' ,beta'] /\ alpha t2<= alpha' /\ beta' t2<= beta}}.
proof: Proof. intros a b Va Vb; case (phi_cases' a Vb). - destruct 1. + case s; intros b1 (b2,(H1,(H2,H3))). rewrite H1 in H3; subst b. exists b1;exists b2;repeat split;auto with T2. + exists a, b;auto with T2. - intros (b1,(b2,(n,(H1,(H2,H3))))); exists a, (gcons b1 b2 0 (fin n));auto with T2. repeat split;auto with T2. subst b;case n;simpl; auto with T2. right;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)