proposition: Lemma maxvar_var : forall t, maxvar t = var t.
proof: Proof. intro t; pattern t; apply term_ind_forall; clear t; intros. refl. rewrite maxvar_fun1, var_fun1. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)