proposition: Lemma red_mod_sub : forall t u s, red_mod E R t u -> red_mod E R (sub s t) (sub s u).
proof: Proof. intros. do 2 destruct H. exists (sub s x); split. apply substitution_closed_rtc. unfold substitution_closed. apply red_sub. hyp. apply red_sub. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)