Problem:
 f X (\x. x) -> h X (\x. x)
 h (f X (\x. x)) (\x. x) -> f (i X) (\x. x)

Proof:
 Higher-Order Church Rosser Processor:
  f X (\x. x) -> h X (\x. x)
  h (f X (\x. x)) (\x. x) -> f (i X) (\x. x)
  critical peaks: 1
   h (h 7 (\x. x)) (\x. x) <-[0,1]-> f (i 7) (\x. x)
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    h (h 7 (\x. x)) (\x. x) *<- h (h 7 (\x. x)) (\x. x) <- . -> f (i 7) (\x. x) ->* 
    h (i 7) (\x. x)
    Qed