Problem:
 f (\x. Z x) (\y. y) -> f (\x. Z x) (\y. Z (Z y))
 f (\x. x) (\y. Z y) -> a

Proof:
 Higher-Order Church Rosser Processor:
  f (\x. Z x) (\y. y) -> f (\x. Z x) (\y. Z (Z y))
  f (\x. x) (\y. Z y) -> a
  critical peaks: 2
   f (\x. x) (\y. y) <-[]-> a
   a <-[]-> f (\x. x) (\y. y)
   
   Higher-Order Closedness Processor:
     all critical pairs are (almost) development closed
    
    Qed