proposition: Lemma subterm_eq_sub u t s : subterm_eq u t -> subterm_eq (sub s u) (sub s t).
proof: Proof. unfold subterm_eq. intro. destruct H as [C]. subst t. exists (subc s C). apply sub_fill. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)