(VAR x) (RULES a -> h(c) a -> h(f(c)) h(f(x)) -> h(f(g(x))) ) (COMMENT from the collection of \cite{Aoto2013})