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