proposition: Lemma term_sub_cont : forall x t, t = sub (single x (Var (var t))) (fill (cont t) (Var x)).
proof: Proof. intros. rewrite sub_fill, subc_cont. unfold single. simpl. rewrite (beq_refl beq_nat_ok). apply term_cont_var. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)