proposition: Lemma symbs_vec_in : forall x t n (ts : terms n), In x (symbs t) -> Vin t ts -> In x (symbs_vec ts).
proof: Proof. induction ts; simpl; intros. contr. destruct H0. subst t. apply in_appl. hyp. apply in_appr. apply IHts; hyp. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)