proposition: Lemma IR_reduction_ordering : monotone -> WF R -> reduction_ordering IR.
proof: Proof. split. apply IR_WF. exact H0. split. apply IR_substitution_closed. apply IR_context_closed. exact H. Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)