(FUN
  f : (o -> o) -> (o -> o) -> o
  a : o
)
(VAR
  x : o
  y : o
  Z : o -> o
)
(RULES
  f (\x. Z x) (\y. y) -> f (\x. Z x) (\y. Z (Z y)),
  f (\x. x) (\y. Z y) -> a
)
(COMMENT Example 4.4 of \cite{AvOS10})