proposition: Lemma hd_red_incl_proj_hd_red : hd_red R << proj_ord (hd_red R').
proof: Proof. unfold inclusion, proj_ord. intros. redtac. subst x. 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)