proposition: Lemma var_cant_be_greater_than_another_term : forall x t, lt_mpo t (Var x) -> False.
proof: Proof. intros x t mpo_t_var_x. inversion mpo_t_var_x. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)