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

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