Problem:
 P (L Z) (\x. Z' x) (\x. Z'' x) -> Z' Z
 P (R Z) (\x. Z' x) (\x. Z'' x) -> Z'' Z

Proof:
 Higher-Order Church Rosser Processor:
  P (L Z) (\x. Z' x) (\x. Z'' x) -> Z' Z
  P (R Z) (\x. Z' x) (\x. Z'' x) -> Z'' Z
  critical peaks: 0
   
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed