Problem:
 g (\x y. F x y (Z x y)) -> C
 g (\x y. F (Z x y) x y) -> C
 g (\x y. F y (Z x y) x) -> C

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