proposition: Lemma red_rev_rtc : forall E t u, red E # t u -> red (reverses E) # (rev' t) (rev' u).
proof: Proof. intros. elim H; intros. apply rt_step. apply red_rev. exact H0. apply rt_refl. eapply rt_trans. apply H1. exact H3. Qed.
imports: CoLoR(Srs ListUtil RelUtil LogicUtil SN)