proposition: Lemma in_vars_subterm_eq : forall x t, List.In x (vars t) -> subterm_eq (Var x) t.
proof: Proof. intros x t. pattern t. apply term_ind_forall; clear t; simpl; intros. intuition. rewrite H0. refl. gen (in_vars_vec_elim H0). intro. destruct H1 as [t]. destruct H1. gen (Vforall_in H H1). intro. gen (H3 H2). intro. apply subterm_strict. eapply subterm_trans_eq1. apply H4. apply subterm_fun. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)