proposition: Lemma rt_red_mod_Frs_Decr : forall E, red (unlab_rules (union Decr (lab_rules E))) # << red E #.
proof: Proof. intro E. trans (red E % #). rewrite red_mod_Frs_Decr. refl. rewrite rc_incl_rtc, rtc_invol. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)