proposition: Lemma red_mod_lab : forall v t u, red_mod E R t u -> red_mod (union Decr E') R' (lab v t) (lab v u).
proof: Proof. intros. do 2 destruct H. ded (rt_red_lab ge_compatE v H). ded (red_lab ge_compatR v H0). do 2 destruct H2. exists x0. intuition. apply rt_trans with (lab v x). eapply incl_elim. apply rt_red_mod_union. hyp. eapply incl_elim. eapply rtc_incl. eapply red_incl. apply subset_union_l. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)