proposition: Lemma acc_mul_acc_wfterms : forall (WM: WFterms), Acc horpo_mul_lt WM -> Acc H_WFterms_lt WM.
proof: Proof. intros WM acc_WM. apply acc_mul_acc_wfmul_aux with (WFterms_to_mul WM); trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)