proposition: Lemma wf_lt : well_founded lt.
proof: Proof. intro s; induction s as [ | f ss HInd1] using term_ind_forall2. apply Acc_lt_var. revert ss HInd1. induction (wf_ltF f) as [f acc_f HInd2]. intros ss Hss; cut (Restricted_acc (Accs lt) (tau f lt) ss). intro Acc_ss; gen Hss; clear Hss. induction Acc_ss as [ss Acc_ss HInd3]. intro Hss; constructor; intro t; induction t as [ | g ts HInd4] using term_ind_forall2; intro H. apply Acc_lt_var. lt_inversion H; try inversion s_is; try inversion t_is; try subst f0 ss0; try subst g0 ts0. apply (HInd2 g ltFfg ts). intros t t_in_ts. apply (HInd4 t t_in_ts). apply (Hsub t t_in_ts). assert (HAccs : Accs lt ts). intros ti ti_in_ts. apply HInd4; trivial. apply Hsub; trivial. assert (H' : Acc lt (Fun f ts)). apply HInd3; trivial. rewrite <- (status_eq g f eqFfg); trivial. apply acc_eq_f with f; trivial; elim eqFfg; split; trivial. subst f0 ts0. gen (Hss t' t'_in_ts); intro acc_t'. elim Ht'; [intro; subst t'; trivial | gen (Fun g ts)]. inversion acc_t'; hyp. apply (status_lifting f). intros s s_in_ss; apply Hss; trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)