proposition: Theorem th_14_6 : forall alpha1 beta1 alpha2 beta2, nf alpha1 -> nf beta1 -> nf alpha2 -> nf beta2 -> phi alpha1 beta1 t2< phi alpha2 beta2 -> {alpha1 t2< alpha2 /\ beta1 t2< phi alpha2 beta2} + {alpha1 = alpha2 /\ beta1 t2< beta2} + {alpha2 t2< alpha1 /\ phi alpha1 beta1 t2< beta2}.
proof: Proof. intros alpha1 beta1 alpha2 beta2 nfa1 nfb1 nfa2 nfb2 E. tricho alpha1 alpha2 H0. - generalize (phi_to_psi alpha2 beta2). intros (gamma1, (gamma2, E')). assert (alpha2 t2<= gamma1). { eapply phi_le; [| eexact E']. auto. } left. left;split;auto. apply le_lt_trans with (phi alpha1 beta1);auto. apply le_b_phi_ab;auto. - subst alpha2;left;right. split;auto. tricho beta1 beta2 H;auto. + subst beta2;case (lt_irr E). + case (lt_not_gt E). apply phi_mono_r;auto. - right; split;auto. generalize (phi_to_psi alpha1 beta1). intros (gamma1, (gamma2, E')). assert (alpha1 t2<= gamma1). { apply phi_le with beta1 gamma2; auto. } assert (alpha2 t2< gamma1). { apply lt_le_trans with alpha1;auto. } assert (phi alpha2 (phi alpha1 beta1) = phi alpha1 beta1). { repeat rewrite E'. cbn. rewrite (compare_rw_lt H1). auto. } assert (phi alpha2 (phi alpha1 beta1) t2< phi alpha2 beta2). eapply le_lt_trans. eleft;eexact H2. auto. apply phi_mono_RR with alpha2;auto. apply phi_nf;auto. 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)