proposition: Lemma lt_eq_f : forall t s, lt s t -> forall f ts, t = Fun f ts -> forall g, g =F= f -> lt s (Fun g ts).
proof: Proof. assert (leF_po : preorder Sig leF). apply leF_preorder. assert (eqF_trans : transitive eqF). elim (eqA_equivalence Sig leF); trivial. intros t; induction t as [ | f ts IHt] using term_ind_forall2. intros s Hs; elim (var_are_min Hs). intro s; induction s as [ | g ss IHs] using term_ind_forall2. intros Hs f' ts' Heq; inversion Heq; subst. lt_inversion Hs; try inversion s_is; try inversion t_is; subst. intros g Hg; apply lt_subterm; exists t'. split; trivial. elim Ht'; clear Ht'; intro Ht'; [subst ; left| right]; trivial. intros Hs f' ts' Heq; inversion Heq; subst. intros g' g'_eq. lt_inversion Hs; try inversion s_is; try inversion t_is; subst. apply lt_roots. apply (ltA_eqA_compat_r Sig leF) with g0; trivial. elim g'_eq; split; trivial. intros t t_in_ss. apply (IHs t t_in_ss (Hsub t t_in_ss) g0 ts); trivial. apply lt_status. apply eqF_trans with g0; trivial. elim eqFfg; split; trivial. intros t t_in_ss. apply (IHs t t_in_ss (Hsub t t_in_ss) g0 ts); trivial. assert (Seq : tau g' = tau f). apply status_eq. apply eqF_trans with g0; trivial. elim eqFfg; split; trivial. rewrite Seq; trivial. apply lt_subterm; exists t'; split; trivial. elim Ht'; [left; subst | right]; trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)