Problem:
 a -> b
 f a -> f b

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