proposition: Lemma vars_fun1 : forall f u, vars (Fun1 f u) = vars u.
proof: Proof. intros. unfold Fun1. rewrite vars_fun, vars_vec_cast. simpl. rewrite <- app_nil_end. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)