proposition: Lemma vars_vec_cast : forall n (ts : terms n) m (h : n=m), vars_vec (Vcast ts h) = vars_vec ts.
proof: Proof. induction ts; intros; destruct m; simpl; try discr. rewrite Vcast_refl. refl. rewrite Vcast_cons. apply (f_equal (fun l => vars h ++ l)). apply IHts. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)