proposition: Lemma WF_red_mod_rev : forall E R, WF (red_mod (reverses E) (reverses R)) -> WF (red_mod E R).
proof: Proof. unfold WF. intros E R H. cut (forall x, SN (red_mod E R) (rev' x)). intros. ded (H0 (rev' x)). rewrite rev'_rev' in H1. exact H1. intro. ded (H x). elim H0. intros. apply SN_intro. intros. ded (H2 (rev' y)). rewrite rev'_rev' in H4. apply H4. ded (red_mod_rev H3). rewrite rev'_rev' in H5. exact H5. Qed.
imports: CoLoR(Srs ListUtil RelUtil LogicUtil SN)