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