proposition: Lemma WF_red_rev_eq : forall R, WF (red (reverses R)) <-> WF (red R).
proof: Proof. intro. rewrite <- !red_mod_empty. assert (nil = reverses nil). refl. rewrite H. apply WF_red_mod_rev_eq. Qed.
imports: CoLoR(Srs ListUtil RelUtil LogicUtil SN)