(FUN
  f : (o -> o) -> (o -> o -> o) -> o
  g : o -> o
  h : o -> o -> o
  a : o
  b : o
)
(VAR
  x : o
  y : o
  Z : o -> o -> o
)
(RULES
  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
)
(COMMENT Example 4.3 of \cite{AvOS10})