proposition: Lemma wf_MulLt_WFterms : well_founded H_WFterms_lt.
proof: Proof. unfold well_founded; intro W. destruct W as [Ts CompTs]. apply acc_mul_acc_wfterms. unfold horpo_mul_lt; apply mOrd_acc. class. intros x x_comp. assert (xComp: CompH x). apply CompTs. destruct (member_multiset_list Ts x_comp). unfold eqA in H0; unfold TermsEqset.eqA in H0; rewrite H0; trivial. apply horpo_comp_imp_acc; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)