proposition: Lemma WF_hd_red_mod_proj : WF (hd_red_mod E' R') -> WF (hd_red_mod E R).
proof: Proof. intro. eapply WF_incl. apply hd_red_mod_proj. apply WF_proj. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)