proposition: Lemma mem_vars_vec : forall x n (ts : terms n), mem x (vars_vec ts) = true -> exists t, Vin t ts /\ mem x (vars t) = true.
proof: Proof. induction ts; simpl; mem; split_all. discr. destruct (orb_true_elim H). exists h. auto. destruct (IHts e). exists x0. tauto. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)