proposition: Lemma filter_comp : forall R : rules, compat succ (filter_rules R) -> compat fsucc R.
proof: Proof. unfold compat. intros. unfold filter_ord. apply H. change (In (filter_rule (mkRule l r)) (filter_rules R)). apply in_map. hyp. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)