proposition: Lemma incl_filter : forall R S, R << S -> filter_ord R << filter_ord S.
proof: Proof. intros. unfold inclusion, filter_ord. intros. apply H. exact H0. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)