Problem:
 h 0 -> g (\x y. x (h y))
 g (\x y. Z (\z. x z) y) -> Z (\z. 0) 0

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