proposition: Lemma in_vars_fun : forall x f ts, List.In x (vars (Fun f ts)) -> exists t, Vin t ts /\ subterm_eq (Var x) t.
proof: Proof. intros. apply subterm_fun_elim. ded (in_vars_subterm_eq _ _ H). apply subterm_noteq. hyp. discr. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)