proposition: Lemma WF_hd_red_Mod_decomp : forall (hypD : rules_preserve_vars D) (cs : decomp) (hyp1 : incl (flat cs) D) (hyp2 : valid_decomp cs = true) (hyp3 : lforall (fun ci => WF (hd_red_Mod S ci)) cs), WF (Union cs).
proof: Proof. induction cs; simpl; intros. apply WF_empty_rel. ded (andb_elim hyp2). clear hyp2. destruct H. destruct hyp3. apply WF_union_commut. hyp. apply IHcs; try hyp. apply incl_appl_incl with a. hyp. clear IHcs H H1 H2. intros t v h. destruct h. destruct H. redtac. rewrite forallb_forall in H0. ded (H0 _ lr). clear H0. destruct (In_Union_elim H1). destruct H0. redtac. rewrite forallb_forall in H2. ded (H2 _ H0). rewrite forallb_forall in H4. ded (H4 _ lr0). rewrite negb_lr in H5. simpl in H5. absurd (Graph (mkRule l r) (mkRule l0 r0)). unfold Graph. rewrite H5. discr. apply approx_correct. apply hd_red_Mod_rule2_hd_rules_graph with (t := t) (u := x) (v := v); unfold hd_red_Mod_rule; subst; intuition. exists s. intuition. eapply incl_flat_In. apply lr0. apply H0. apply incl_appl_incl with a. hyp. exists s0. intuition. Qed.
imports: CoLoR(AGraph Union ATrs RelUtil ListUtil LogicUtil SN BoolUtil VecUtil)