λR. ∀ x, R x x

Definition reflexive : forall (A:Type), (A -> A -> Prop) -> Prop := fun (A:Type) => fun (R:(A -> A -> Prop)) => forall (x:A), R x x

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

def reflexive : forall (A : Type) , ((A) -> (A) -> Prop) -> Prop := fun (A : Type) , fun (R : (A) -> (A) -> Prop) , forall (x:A) , ((R) (x)) (x)

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

Printing for OpenTheory is not working at the moment.