proposition: Lemma vars_vec_app : forall n1 (ts1 : terms n1) n2 (ts2 : terms n2), vars_vec (Vapp ts1 ts2) = vars_vec ts1 ++ vars_vec ts2.
proof: Proof. induction ts1; intros; simpl. refl. rewrite app_ass. f_equal. apply IHts1. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)