(VAR x y z) (RULES a(b(x)) -> a(c(b(x))) ) (COMMENT Example 4.35 in \cite{SK90})