proposition: Lemma hd_red_lab : forall v t u, hd_red R t u -> hd_red_mod Decr R' (lab v t) (lab v u).
proof: Proof. intros. redtac. subst. exists (lab v (sub s l)). split. apply rt_refl. rewrite !lab_sub_eq. exists (lab (beta v s) l). exists (lab (beta v s) r). exists (lab_sub v s). intuition. exists (mkRule l r). exists (beta v s). intuition. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)