proposition: Lemma compat_hd_red_mod : forall R E, substitution_closed succ -> rewrite_ordering succ_eq -> compat succ_eq E -> compat succ R -> absorbs_left succ succ_eq -> hd_red_mod E R << succ.
proof: Proof. intros. unfold hd_red_mod. incl_trans (succ_eq# @ succ). comp. apply rtc_incl. apply compat_red; hyp. apply compat_hd_red; hyp. apply absorbs_left_rtc. exact H3. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)