Problem:
 mu (\x. z x) -> z (mu (\x. z x))

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