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