proposition: Lemma hd_rule_partition_complete : forall pf (R : rules), let part := partition pf R in hd_red R << hd_red (fst part) U hd_red (snd part).
proof: Proof. clear R. intros. incl_trans (hd_red (fst part ++ snd part)). apply hd_red_incl. unfold incl. intros. destruct (partition_complete pf a R). hyp. apply in_or_app. auto. apply in_or_app. auto. apply hd_red_union. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)