(FUN
  f : o -> (o -> o) -> o
  g : o -> o -> o
  a : o
  b : o
)
(VAR
  F : o -> o
  X : o
  x : o
)
(RULES
  f(X,\x.F(x)) -> F(X),
  g(a,a) -> f(a,\x.g(b,x)),
  b -> a
)
(COMMENT Example 7 from \cite{SK05})