proposition: Lemma proj_comp : forall R : rules, compat succ (proj_rules R) -> compat psucc R.
proof: Proof. unfold compat. intros. unfold proj_ord. apply H. change (In (proj_rule (mkRule l r)) (proj_rules R)). apply in_map. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)