proposition: Lemma acc_mul_acc_wfmul_aux : forall (M: Multiset), Acc horpo_mul_lt M -> forall (WM: WFterms), M = WM -> Acc H_WFterms_lt WM.
proof: Proof. intros M AccM. apply Acc_ind with (R := MultisetLT horpo) (P := fun M => forall (WM: WFterms), M = WFterms_to_mul WM -> Acc H_WFterms_lt WM). intros x acc_mul acc_WM WM x_WM. constructor. intros y y_lt_WM. apply acc_WM with (WFterms_to_mul y). rewrite x_WM. trivial. trivial. trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)