proposition: Lemma in_vars_vec_elim : forall x n (ts : terms n), In x (vars_vec ts) -> exists t, Vin t ts /\ In x (vars t).
proof: Proof. induction ts; simpl; intros. contr. gen (in_app_or H). intro. destruct H0. exists h. intuition. gen (IHts H0). intro. destruct H1 as [t]. exists t. intuition. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)