proposition: Lemma var_sub : forall s t, var (sub s t) = var (s (var t)).
proof: Proof. intro s. apply term_ind_forall. refl. intros. rewrite sub_fun1, !var_fun1. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)