proposition: Lemma compat_red_mod_tc : forall R E, rewrite_ordering succ -> compat E -> compat R -> red_mod E R << succ!.
proof: Proof. intros. unfold red_mod. incl_trans (succ# @ succ). comp. apply rtc_incl. apply compat_red; hyp. apply compat_red; hyp. apply tc_split_inv. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)