λx. λy. ∀ P, P x ⇒ P y

Definition leibniz : forall (A:Type), A -> A -> Prop := fun (A:Type) => fun (x:A) => fun (y:A) => forall (P:(A -> Prop)), (P x) -> P y

definition leibniz : \forall A : Type[0] . A -> A -> Prop := \lambda A : Type[0]. \lambda x : A. \lambda y : A. \forall (P:A -> Prop). (P x) -> P y

def leibniz : forall (A : Type) , (A) -> (A) -> Prop := fun (A : Type) , fun (x : A) , fun (y : A) , forall (P:(A) -> Prop) , ((P) (x)) -> (P) (y)

leibniz [A:TYPE+] : [A -> [A -> bool]] = (LAMBDA(x:A):(LAMBDA(y:A):(FORALL(P:[A -> bool]):(P(x) => P(y)))))

Printing for OpenTheory is not working at the moment.