proposition: Lemma Fred_mod : forall E R t u, red_mod E R t u -> red_mod (Frs E) (Frs R) (Ft t) (Ft u).
proof: Proof. intros. redtac. unfold red_mod. exists (Ft t0). split. apply Fred_rtc. hyp. apply Fred. subst. apply red_rule. hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)