proposition: Lemma IR_rewrite_ordering : forall succ, monotone I succ -> rewrite_ordering (IR I succ).
proof: Proof. split. apply IR_substitution_closed. apply IR_context_closed. hyp. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)