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