proposition: Lemma decomp_incl : forall cs (hyp1 : incl D (flat cs)), hd_red_Mod S D << Union cs.
proof: Proof. intros. intros x y h. redtac. ded (hyp1 _ lr). revert H0. elim cs; simpl; intros. contr. destruct (in_app_or H1). left. exists t. intuition. subst. apply hd_red_rule. hyp. right. apply H0. hyp. Qed.
imports: CoLoR(AGraph Union ATrs RelUtil ListUtil LogicUtil SN BoolUtil VecUtil)