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