proposition: Lemma compat_red : forall R, rewrite_ordering succ -> compat R -> red R << succ.
proof: Proof. intro. unfold inclusion. intros (Hsubs,Hcont) Hcomp u v H. redtac. subst u. subst v. apply Hcont. apply Hsubs. apply Hcomp. hyp. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)