proposition: Lemma rule_partition_complete : forall pf (R : rules), let part := partition pf R in red R << red (fst part) U red (snd part).
proof: Proof. clear R. intros. apply red_partition. intros. unfold part. apply partition_complete. hyp. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)