proposition: Lemma Fred_mod_WF : forall E R, WF (red_mod (Frs E) (Frs R)) -> WF (red_mod E R).
proof: Proof. intros E R H x. geneq H x (Ft x). induction 1; intros. apply SN_intro; intros. eapply H0. subst x. apply Fred_mod. apply H2. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)