proposition: Lemma is_compat_correct : forall R, is_compat R = true -> compat R /\ is_compat R = false -> ~compat R.
proof: Proof. induction R; simpl. intuition. destruct a. case (succ_dec lhs rhs); intros; destruct H0; ded (compat_cons_elim H0); intuition. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)