proposition: Lemma hd_red_mod_proj : hd_red_mod E R << proj_ord (hd_red_mod E' R').
proof: Proof. unfold inclusion, proj_ord. intros. redtac. exists (proj t). split. apply red_rtc_incl_proj_red_rtc. exact H. subst t. subst y. rewrite !proj_sub. apply hd_red_rule. change (In (proj_rule (mkRule l r)) R'). apply in_map. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)