Le terme (fun  (x)  fun  (y)  y convient. En effet:

(fun  (z)  fun  (t)  fun  (f)  (z t) f) (fun  (x)  fun  (y)  y) 1 2 ® ... ( (fun  (x)  fun  (y)  y) 1 2) ® ((fun  (y)  y) {x ¬ 1}) 2) º (fun  (y)  y) 2 ® y {y ¬ 2} º 2

On vérifie:

(fun z t f -> (z t) f) (fun x y -> y) 1 2;; - : int = 2

Le terme (fun  (z)  fun  (t)  fun  (f)  (z t) f) se comporte comme if _  then  _  else _ et les termes (fun  (x)  fun  (y)  x) et (fun  (x)  fun  (y)  y) comme true  et false , respectivement.