proposition: Lemma reset_fun1 : forall f t, reset (Fun1 f t) = Fun1 f (reset t).
proof: Proof. intros. unfold reset. rewrite var_fun1, sub_fun1. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)