(VAR x y)
(HORN-CLAUSES
  x === y | x ->* y
)
(RULES
  a -> b
  f(x) -> c | x === a
)
(COMMENT
  Example 2, item 1, Lucas JLAMP'24
  
)
