proposition: Lemma WF_hd_red_mod_lab_fin : WF (hd_red_mod E R) <-> WF (hd_red_mod (D' ++ E') R').
proof: Proof. rewrite <- !hd_red_mod_Rules, WF_hd_red_mod_lab. 2: apply ge_compatE. apply WF_same. rewrite of_app, Rules_enum_Decr, !lab_rules_enum. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)