λR. λf. ∀ x y, R x y ⇒ R (f x) (f y)

Definition monotonic : forall (A:Type), (A -> A -> Prop) -> (A -> A) -> Prop := fun (A:Type) => fun (R:(A -> A -> Prop)) => fun (f:(A -> A)) => forall (x:A), forall (y:A), (R x y) -> R (f x) (f y)

definition monotonic : \forall A : Type[0] . (A -> A -> Prop) -> (A -> A) -> Prop := \lambda A : Type[0]. \lambda R : A -> A -> Prop. \lambda f : A -> A. \forall (x:A). \forall (y:A). (R x y) -> R (f x) (f y)

def monotonic : forall (A : Type) , ((A) -> (A) -> Prop) -> ((A) -> A) -> Prop := fun (A : Type) , fun (R : (A) -> (A) -> Prop) , fun (f : (A) -> A) , forall (x:A) , forall (y:A) , (((R) (x)) (y)) -> ((R) ((f) (x))) ((f) (y))

monotonic [A:TYPE+] : [[A -> [A -> bool]] -> [[A -> A] -> bool]] = (LAMBDA(R:[A -> [A -> bool]]):(LAMBDA(f:[A -> A]):(FORALL(x:A):(FORALL(y:A):(R(x)(y) => R(f(x))(f(y)))))))

Printing for OpenTheory is not working at the moment.