⁴Indeed, the correctness of the _.=._ predicate does not depend on an explicit declaration of constructors in a module; it only depends on the associated equational theory being ground confluent and terminating.