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

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