proposition: Lemma wf_lt_mpo : well_founded lt_mpo.
proof: Proof. intro s; induction s as [ | f ss HInd1] using term_ind_forall2. apply Acc_lt_mpo_var. revert ss HInd1. induction (wf_ltF f) as [f acc_f HInd2]. intros ss HInd3; cut (Acc (mult (transp lt_mpo)) ss). intro Acc_ss; gen HInd3; clear HInd3. induction Acc_ss as [ss Acc_ss HInd3]. constructor; intro t; induction t as [ | g ts HInd4] using term_ind_forall2; intro H. apply Acc_lt_mpo_var. inversion H as [f' g' ss' ts' ltFfg Hsi' | f' ss' ts' Hss'ts' Hsi' | f' s' ts' Hex]; subst. apply (HInd2 g ltFfg ts). intros t t_in_ts. apply (HInd4 t t_in_ts). apply (Hsi' t t_in_ts). cut (forall t : term, In t ts -> Acc lt_mpo t); [intro acc_t | intros t t_in_ts]. apply (HInd3 ts); try hyp. apply (HInd4 t t_in_ts). apply transitive_lt_mpo with (Fun f ts); trivial. apply strict_subterm_less; hyp. elim Hex; clear Hex; intros s Hs; elim Hs; clear Hs; intros s_in_ss MPO_s_t. gen (HInd0 s s_in_ss); intro Acc_s. elim MPO_s_t; [intro; subst s; trivial | gen (Fun g ts)]. inversion Acc_s; hyp. apply (HAccTermsToTermlist (transp lt_mpo) tlt_mpo_eqA_compat IN_eqA_compat). intros s s_in_ss; gen (HInd3 s s_in_ss). rewrite transp_invol. auto. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)