Problem:
 compo (\x. F x) (\y. G y) Z -> F (G Z)
 apply (\x. F x) X -> F X

Proof:
 Modularity Decomposition: 
 0:compo (\x. F x) (\y. G y) Z -> F (G Z)
 1:apply (\x. F x) X -> F X
 -----
 0:compo (\x. F x) (\y. G y) Z -> F (G Z)
   Higher-Order Church Rosser Processor:
    compo (\x. F x) (\y. G y) Z -> F (G Z)
    critical peaks: 0
     
     
     Higher-Order Closedness Processor:
       all critical pairs are trivial
      
      Qed
   
   
   1:apply (\x. F x) X -> F X
     Higher-Order Church Rosser Processor:
      apply (\x. F x) X -> F X
      critical peaks: 0
       
       
       Higher-Order Closedness Processor:
         all critical pairs are trivial
        
        Qed