proposition: Lemma red_mod_rev : forall E R t u, red_mod E R t u -> red_mod (reverses E) (reverses R) (rev' t) (rev' u).
proof: Proof. intros. redtac. exists (rev' (fill c l)). split. apply red_rev_rtc. exact H. apply red_rev. exists l. exists r. exists c. auto. Qed.
imports: CoLoR(Srs ListUtil RelUtil LogicUtil SN)