proposition: Lemma term_cont_var : forall t, t = fill (cont t) (Var (var t)).
proof: Proof. apply term_ind_forall. refl. intros. rewrite cont_fun1, fill_cont1, var_fun1, <- H. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)