We consider termination of the STRS with no additional rule schemes:

  Signature: fapp :: o -> o -> o
             h    :: o -> o
             lam  :: (o -> o) -> o

  Rules: fapp(lam(X), Y) -> X(h(Y))

The system does not satisfy the preconditions to apply static dependency pairs: it is not accessible function passing.

No HORPO proof could be found.