proposition: Lemma var_reset : forall t, var (reset t) = 0.
proof: Proof. intro t; pattern t; apply term_ind_forall; clear t; intros. unfold reset, swap, single. simpl. rewrite (beq_refl beq_nat_ok). refl. unfold reset. rewrite sub_fun1, !var_fun1. fold (reset t). hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)