proposition: Lemma red_partition : forall (R R1 R2 : rules), (forall r, In r R -> In r R1 \/ In r R2) -> red R << red R1 U red R2.
proof: Proof. Proof with auto. intros. incl_trans (red (R1 ++ R2)). apply red_incl. unfold incl. intros. destruct (H a); solve [hyp | apply in_or_app; auto]. apply red_union. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)