proposition: Lemma WF_red_lab_fin : WF (red R) <-> WF (red_mod D' R').
proof: Proof. rewrite <- red_Rules, <- red_mod_Rules, WF_red_lab. 2: apply ge_compatR. apply WF_same. rewrite 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)