proposition: Lemma vars_var : forall t, vars t = var t :: nil.
proof: Proof. apply term_ind_forall. refl. intros. rewrite vars_fun1, var_fun1. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)