proposition: Lemma rt_red_Frs_Decr : red (unlab_rules Decr) # << @eq term.
proof: Proof. intros t u. induction 1. apply red_Frs_Decr. hyp. refl. trans y; hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)