proposition: Lemma maxvar_fun1 : forall f t, maxvar (Fun1 f t) = maxvar t.
proof: Proof. intros. unfold Fun1. rewrite maxvar_fun, maxvars_cast. unfold maxvars. simpl Vmap. simpl VecMax.Vmax. rewrite max_0_r. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)