Problem:
 app (abs (\x. z x)) y -> z y
 abs (\x. app y x) -> y
 app bot x -> bot
 abs (\x. bot) -> bot

Proof:
 Higher-Order Church Rosser Processor:
  app (abs (\x. z x)) y -> z y
  abs (\x. app y x) -> y
  app bot x -> bot
  abs (\x. bot) -> bot
  critical peaks: 4
   abs (\13. 12 13) <-[1,0]-> abs (\11. 12 11)
   app 31 y <-[0,1]-> app 31 y
   abs (\x. bot) <-[1,0]-> bot
   app bot y <-[0,1]-> bot
   
   Higher-Order Closedness Processor:
     all critical pairs are (almost) development closed
    
    Qed