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

Proof:
 Higher-Order Church Rosser Processor:
  f (g (\x. z x)) -> f (z (z a))
  g (\x. h' x) -> h (h a)
  h x -> h' x
  critical peaks: 1
   f (h (h a)) <-[1]-> f (h' (h' a))
   
   Higher-Order Closedness Processor:
     all critical pairs are (almost) development closed
    
    Qed