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

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