proposition: Lemma WF_red_lab : WF (red R) <-> WF (red_mod Decr (lab_rules R)).
proof: Proof. rewrite WF_red_lab_fin. refl. apply pi_mon. apply I_mon. apply Is_ok. apply Fs_ok. apply L2s_ok. apply bge_ok. apply bge_compatR. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)