sub.pcf

(FIX sub.\x.\y.
  IFZ y
    THEN x
    ELSE\yy.IFZ x
             THEN Z
             ELSE\xx.sub xx yy
 : *->*->*)
  (SSSSZ)
  (SSZ)