proposition: Lemma red_monotonous : forall R, monotonous (Reduction R).
proof: Proof. intro R. apply monotonicity_criterion. intros; apply RedAppL with Mapp M'app; trivial. intros; apply RedAppR with Mapp M'app; trivial. intros; apply RedAbs with Nabs N'abs; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubstConv)