proposition: Lemma rule_partition_compat : forall succ (succ_dec : rel_dec succ), snd (partition (rule_partition succ_dec) R) = nil -> compat succ R.
proof: Proof. intros. intros l r Rlr. apply partition_by_rel_true with term succ_dec. apply rule_partition_left with R. destruct (partition_complete (rule_partition succ_dec) (mkRule l r) R). hyp. hyp. rewrite H in H0. destruct H0. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)