proposition: Lemma red_Frs_Decr : red (unlab_rules Decr) << @eq term.
proof: Proof. intros t u h. redtac. subst. destruct lr as [[l' r'] [h1 h2]]. destruct h1 as [f [a [b [ab h]]]]. inversion h. subst. inversion h2. assert (HF (mk a) = HF (mk b)). apply UIP. apply eq_nat_dec. rewrite H. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)