Problem:
 f z -> z
 h' (\x. h (f (g x))) -> a

Proof:
 Higher-Order Church Rosser Processor:
  f z -> z
  h' (\x. h (f (g x))) -> a
  critical peaks: 1
   h' (\x. h (g x)) <-[1,0,1]-> a
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    h' (\x. h (g x)) *<- h' (\x. h (g x)) <- . -> a ->* a
    Qed