proposition: Lemma partition_succ_compat : forall R, compat IR_succ (fst (partition part_succ R)).
proof: Proof. intros R l r lr. apply succ'_sub. apply partition_by_rel_true with MA.term succ'_dec. apply rule_partition_left with R. hyp. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)