proposition: Lemma WF_red_mod_lab_fin : WF (red_mod E R) <-> WF (red_mod (D' ++ E') R').
proof: Proof. rewrite <- !red_mod_Rules, WF_red_mod_lab. 2: apply ge_compatE. 2: apply ge_compatR. 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)