Problem:
 app (abs (\y. X y)) Y -> sub (\y. X y) Y
 sub (\y. X0) Y -> X0
 sub (\y. y) Y -> Y
 sub (\y. abs (\x. X2 x y)) Y -> abs (\x. sub (\y. X2 x y) Y)
 sub (\y. app (X y) (X' y)) Y -> app (sub (\y. X y) Y) (sub (\y. X' y) Y)

Proof:
 Higher-Order Church Rosser Processor:
  app (abs (\y. X y)) Y -> sub (\y. X y) Y
  sub (\y. X0) Y -> X0
  sub (\y. y) Y -> Y
  sub (\y. abs (\x. X2 x y)) Y -> abs (\x. sub (\y. X2 x y) Y)
  sub (\y. app (X y) (X' y)) Y -> app (sub (\y. X y) Y) (sub (\y. X' y) Y)
  critical peaks: 5
   sub (\y. sub (\16. 17 y 16) (18 y)) Y <-[0,1,0]->
     app (sub (\y. abs (\15. 17 y 15)) Y) (sub (\y. 18 y) Y)
   abs (\x. 45 x) <-[]-> abs (\x. sub (\47. 45 x) 46)
   app 56 57 <-[]-> app (sub (\59. 56) 58) (sub (\60. 57) 58)
   abs (\x. sub (\90. 88 x) 89) <-[]-> abs (\x. 88 x)
   app (sub (\125. 122) 124) (sub (\126. 123) 124) <-[]-> app 122 123
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    sub (\y. sub (\16. 17 y 16) (18 y)) Y *<- sub (\y. sub (\16. 17 y 16) (18 y)) Y <- . -> 
    app (sub (\y. abs (\15. 17 y 15)) Y) (sub (\y. 18 y) Y) ->* sub (\y. sub (\208. 17 208 y) Y)
                                                                (sub (\y. 18 y) Y)
    Qed