proposition: Lemma var_in : forall x t, lt (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. lt_inversion H; try inversion t_is. lt_inversion H; try inversion t_is; try inversion s_is. constructor; exists t'; split; trivial. subst; elim Ht'; clear Ht'; intro Ht'. subst; constructor. apply IHt; trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)