proposition: Lemma Acc_lt_mpo_var : forall x, Acc lt_mpo (Var x).
proof: Proof. intro x; constructor; intros t lt_mpo_t_var_x. elim (var_cant_be_greater_than_another_term x t); hyp. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)