proposition: Lemma rt_red_lab : forall v t u, red R # t u -> red_mod Decr R' # (lab v t) (lab v u).
proof: Proof. induction 1. apply rt_step. apply red_lab. hyp. apply rt_refl. apply rt_trans with (lab v y); hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)