(FUN
  f : o -> o -> o
  g : o -> o -> o
  a : o
  b : o
  h : (o -> o) -> o
)
(VAR
  x : o
  F : (o -> o)
)
(RULES
  f x b -> g x x,
  g x a -> f x x,
  h (\x. F(x)) -> F(a),
  h (\x. F(x)) -> F(b)
)
(COMMENT from \cite{FK11}, p 10)