proposition: Theorem th_14_5 : forall alpha1 beta1 alpha2 beta2, nf alpha1 -> nf beta1 -> nf alpha2 -> nf beta2 -> phi alpha1 beta1 = phi alpha2 beta2 -> {alpha1 t2< alpha2 /\ beta1 = phi alpha2 beta2} + {alpha1 = alpha2 /\ beta1 = beta2} + {alpha2 t2< alpha1 /\ phi alpha1 beta1 = 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. assert (phi alpha1 (phi alpha2 beta2) = phi alpha2 beta2). { repeat rewrite E'. cbn. generalize (lt_le_trans H0 H);intro H1. rewrite (compare_rw_lt H1). auto. } pattern (phi alpha2 beta2) at 2 in H1. rewrite <- E in H1. apply phi_inj_r with alpha1;auto. apply phi_nf;auto. - subst alpha2; left; right. split;auto. apply phi_inj_r with alpha1;auto. - generalize (phi_to_psi alpha1 beta1). intros (gamma1, (gamma2, E')). assert (alpha1 t2<= gamma1). { apply phi_le with beta1 gamma2; auto. } right. split;auto. assert (phi alpha2 (phi alpha1 beta1) = phi alpha1 beta1). { repeat rewrite E'. cbn; generalize (lt_le_trans H0 H);intro H1. rewrite (compare_rw_lt H1). auto. } pattern (phi alpha1 beta1) at 2 in H1. rewrite E in H1. apply phi_inj_r 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)