Determine if a given tree is a binary search tree with lambda calculus

Question

can anyone help me to find out how to make a function that return true if a tree is a BST.

Definition binTree (A : Set) : Set := forall T : Set, T -> (T -> A -> T -> T) -> T. 

Definition pET (A : Set) : binTree A := fun (T : Set) (x : T) (c : T -> A -> T -> T) => x. 

Definition pNT (A : Set) (g : binTree A) (a : A) (d : binTree A) : binTree A :=
  fun (T : Set) (x : T) (c : T -> A -> T -> T) => c (g T x c) a (d T x c).

I have tried this one , but that does not work.

function (isInf a b ) return true if a <= b

function (and a b) return ( a && b)

Definition is_BST ( t : binTree nat ) : bool :=
   t bool true ( fun left racine right =>  (and (isInf left racine) ( isInf racine right))).