Problem:
 f1 X -> f2 X X
 f2 a X -> f3 X
 g1 (\x. f3 (F x)) -> F (hide (\x. f3 (F x)))
 unhide (hide (\x. F x)) -> g2 (\x. F x)
 g2 (\x. f3 (F x)) -> g1 (\x. f1 (F x))

Proof:
 Higher-Order Church Rosser Processor:
  f1 X -> f2 X X
  f2 a X -> f3 X
  g1 (\x. f3 (F x)) -> F (hide (\x. f3 (F x)))
  unhide (hide (\x. F x)) -> g2 (\x. F x)
  g2 (\x. f3 (F x)) -> g1 (\x. f1 (F x))
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed