proposition: Lemma WF_red_unlab_fin : forall R, WF (red (unlab_rules_fin R)) -> WF (red R).
proof: Proof. intros. apply Fred_WF_fin with (S2:=Sig) (F:=F) (HF:=HF). hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)