Problem:
 f x b -> g x x
 g x a -> f x x
 h (\x. F x) -> F a
 h (\x. F x) -> F b

Proof:
 Higher-Order Church Rosser Processor:
  f x b -> g x x
  g x a -> f x x
  h (\x. F x) -> F a
  h (\x. F x) -> F b
  critical peaks: 2
   13 a <-[]-> 13 b
   17 b <-[]-> 17 a
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    13 a *<- 13 a <- . -> 13 b ->* 13 b
    Qed