Problem:
 f (\x. x) (\x y. Z x y) -> g (Z a (f (\x. Z x a) (\x y. Z x y)))
 h x y -> x

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