proposition: Lemma red_mod_ren : forall t u, red_mod E R (sub s t) u -> exists v, red_mod E R t v /\ sub s v = u.
proof: Proof. intros. do 2 destruct H. destruct (rtc_red_ren hE H). destruct H1. subst. destruct (red_ren hR H0). exists x. split_all. exists x0. intuition. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)