proposition: Lemma compat_cons : forall l r R, succ l r -> compat R -> compat (mkRule l r :: R).
proof: Proof. unfold compat. simpl. intros. destruct H1. injection H1. intros. subst l0. subst r0. exact H. apply H0. exact H1. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)