Problem:
 f (\x y. F (\z. x z) y) -> h (F (\z. g z) a) (F (\z. g z) a)
 g a -> f (\x y. h (x a) y)

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