(FUN
  f : (a -> a) -> a
  d : a
)
(VAR
  F : a -> a
  x : a
)
(RULES
  f(\x.F(x)) -> F(f(\x. d))
)
(COMMENT Example 14 from \cite{SWS01})