proposition: Lemma ma_compat_hd_red_mod : compat IR_succ R -> compat IR_succeq E -> WF (hd_red_mod E R).
proof: Proof. intros. apply WF_incl with IR_succ. apply compat_hd_red_mod with IR_succeq; trivial. apply IR_substitution_closed. exact ma_succeq_rewrite_ordering. exact absorb_succ_succeq. apply IR_WF. exact succ_wf. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)