proposition: Lemma subterm_sub u t s : subterm u t -> subterm (sub s u) (sub s t).
proof: Proof. unfold subterm. intro. destruct H as [C]. intuition. destruct C. intuition. subst t. exists (subc s (Cont f e t0 C t1)). split_all. discr. apply sub_fill. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)