Problem:
 app (abs (\x. F x)) S -> F S
 abs (\x. app S x) -> S

Proof:
 Higher-Order Church Rosser Processor:
  app (abs (\x. F x)) S -> F S
  abs (\x. app S x) -> S
  critical peaks: 2
   abs (\13. 12 13) <-[1,0]-> abs (\11. 12 11)
   app 23 S <-[0,1]-> app 23 S
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed