proposition: Lemma red_subterm : forall u u' t, red R u u' -> subterm_eq u t -> exists t', red R t t' /\ subterm_eq u' t'.
proof: Proof. unfold subterm_eq. intros. destruct H0 as [d]. subst t. redtac. subst u. subst u'. exists (fill (AContext.comp d c) (sub s r)). split. ex l r (AContext.comp d c) s. split. hyp. rewrite fill_fill. auto. exists d. rewrite fill_fill. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)