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

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