proposition: Lemma WF_red_lab : WF (red R) <-> WF (red_mod Decr R').
proof: Proof. split; intro. apply Fred_mod_WF with (S2:=Sig) (F:=F) (HF:=HF). apply WF_incl with (red R). 2: hyp. intros t u h. redtac. ded (rt_red_Frs_Decr H0). subst t0. subst. apply red_rule. eapply Frs_iso. hyp. set (v := fun x : variable => some_elt I). apply WF_incl with (Rof (red_mod Decr R') (lab v)). intros t u h. unfold Rof. apply red_lab. hyp. apply WF_inverse. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)