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

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