proposition: Lemma psi_principal : forall a b c d, nf c -> c t2< [a, b] -> d t2< [a, b] -> c + d t2< [a, b].
proof: Proof. induction c;destruct d;simpl;auto with T2. case (compare [c1,c2][d1,d2]). - intros;apply psi_lt_head; inversion_clear H0. + constructor 2;auto with T2. + constructor 3;auto with T2. + constructor 4;auto with T2. + constructor 5;auto with T2. + inversion H2. + inversion H2. - auto with T2. - intros H H0 H1. generalize (IHc3 (gcons d1 d2 n0 d3)); intros H2. assert (H5 : c3 t2< [a,b]). { eapply lt_trans; [| eexact H0]. apply lt_tail. auto with T2. } inversion_clear H0. + constructor 2;auto with T2. + constructor 3;auto with T2. + constructor 4;auto with T2. + constructor 5;auto with T2. + inversion H3. + constructor 7;auto with T2. inversion H3. 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)