proposition: Lemma hd_red_mod_filter : hd_red_mod E R << filter_ord (hd_red_mod E' R').
proof: Proof. unfold inclusion, filter_ord. intros. redtac. exists (filter t). split. apply red_rtc_incl_filter_red_rtc. exact H. subst t. subst y. rewrite !filter_sub. apply hd_red_rule. change (In (filter_rule (mkRule l r)) R'). apply in_map. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)