proposition: Lemma WF_hd_red_mod_lab : WF (hd_red_mod E R) <-> WF (hd_red_mod (union Decr E') R').
proof: Proof. split; intro. apply Fhd_red_mod_WF with (S2:=Sig) (F:=F) (HF:=HF). apply WF_incl with (hd_red_mod E R). 2: hyp. intros t u h. destruct h. destruct H0. apply rt_red_mod_Frs_Decr in H0. exists x. intuition. apply incl_elim with (R:=hd_red (Frs HF R')). rewrite Frs_iso. refl. hyp. set (v := fun x : variable => some_elt I). apply WF_incl with (Rof (hd_red_mod (union Decr E') R') (lab v)). intros t u h. unfold Rof. apply hd_red_mod_lab. hyp. apply WF_inverse. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)