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