proposition: Lemma compat_lforall : forall R, lforall compat_rule R -> compat R.
proof: Proof. induction R; unfold compat; simpl; intros. contr. intuition. subst a. exact H1. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)