proposition: Lemma red_mod_Frs_Decr : forall E, red (unlab_rules (union Decr (lab_rules E))) << red E %.
proof: Proof. intros E t u h. redtac. subst. apply Frs_app in lr. destruct lr. left. eapply rt_red_Frs_Decr. apply rt_step. apply red_rule. hyp. right. apply red_rule. do 2 destruct H. rewrite H0. clear H0. do 3 destruct H. subst. destruct x0. simpl. rewrite !Ft_epi. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)