proposition: Lemma in_var : forall x t, t <> Var x -> in_term_vars x t -> lt (Var x) t.
proof: Proof. intros x t; induction t as [y| f ts IHt] using term_ind_forall2; intros Hneq H; inversion H. elim Hneq; subst; trivial. subst. elim H2; clear H2; intros s Hs; elim Hs; clear Hs; intros s_in_ss Hs. apply lt_subterm; exists s; split; trivial. elim (term_eq_dec s (Var x)); intro case_s. left; trivial. right; apply (IHt s s_in_ss case_s Hs). Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)