Problem:
 g (\y. X (\x. y x)) -> X (\z. X (\x. z))
 f (\x. Y x) -> dots

Proof:
 Modularity Decomposition: 
 0:g (\y. X (\x. y x)) -> X (\z. X (\x. z))
 1:f (\x. Y x) -> dots
 -----
 0:g (\y. X (\x. y x)) -> X (\z. X (\x. z))
   Higher-Order Church Rosser Processor:
    g (\y. X (\x. y x)) -> X (\z. X (\x. z))
    critical peaks: 0
     
     
     Higher-Order Closedness Processor:
       all critical pairs are trivial
      
      Qed
   
   
   1:f (\x. Y x) -> dots
     Higher-Order Church Rosser Processor:
      f (\x. Y x) -> dots
      critical peaks: 0
       
       
       Higher-Order Closedness Processor:
         all critical pairs are trivial
        
        Qed