proposition: Lemma WF_hd_red_mod_filter : WF (hd_red_mod E' R') -> WF (hd_red_mod E R).
proof: Proof. intro. eapply WF_incl. apply hd_red_mod_filter. apply WF_filter. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)