proposition: Lemma WF_decomp : forall (hypD : rules_preserve_vars D) (cs : decomp) (hyp1 : incl D (flat cs)) (hyp2 : incl (flat cs) D) (hyp3 : valid_decomp cs = true) (hyp4 : lforall (fun ci => WF (hd_red_Mod S ci)) cs), WF (hd_red_Mod S D).
proof: Proof. intros. apply WF_incl with (Union cs). apply decomp_incl. hyp. apply WF_hd_red_Mod_decomp; hyp. Qed.
imports: CoLoR(AGraph Union ATrs RelUtil ListUtil LogicUtil SN BoolUtil VecUtil)