Problem:
 f (g (\x. F x)) -> F (g (\x. h (F x)))

Proof:
 Higher-Order Church Rosser Processor:
  f (g (\x. F x)) -> F (g (\x. h (F x)))
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed