proposition: Lemma var_in : forall x t, lt_mpo (Var x) t -> in_term_vars x t.
proof: Proof. intros x t; induction t as [y| f ts IHt] using term_ind_forall2; intro H; inversion H; subst. elim H2; clear H2; intros t Ht; elim Ht; clear Ht; intros t_in_ts Ht. constructor; exists t; split; trivial. elim Ht; clear Ht; intro Ht. subst; constructor. apply IHt; trivial. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)