Problem:
 f a x -> f b x
 a -> b
 b -> c

Proof:
 Higher-Order Church Rosser Processor:
  f a x -> f b x
  a -> b
  b -> c
  critical peaks: 1
   f b x <-[0,1]-> f b x
   
   Higher-Order Closedness Processor:
     all critical pairs are trivial
    
    Qed