proposition: Lemma WF_red_mod_rev_eq : forall E R, WF (red_mod (reverses E) (reverses R)) <-> WF (red_mod E R).
proof: Proof. split; intro. apply WF_red_mod_rev. hyp. apply WF_red_mod_rev. rewrite !reverses_reverses. hyp. Qed.
imports: CoLoR(Srs ListUtil RelUtil LogicUtil SN)