proposition: Lemma compat_cons_elim : forall l r R, compat (mkRule l r :: R) -> succ l r /\ compat R.
proof: Proof. unfold compat. simpl. intros. split; intros; apply H; intuition. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)