proposition: Lemma in_var : forall x t, in_term_vars x t -> le_mpo (Var x) t.
proof: Proof. intros x t; induction t as [y| f ts IHt] using term_ind_forall2; intro H; inversion H; subst. left; trivial. elim H2; clear H2; intros s Hs; elim Hs; clear Hs; intros s_in_ss Hs. right; constructor 3; exists s; split; trivial. elim (IHt s s_in_ss Hs); intro caseIHt; [left; subst; trivial | right; hyp]. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)