% From The Art of Eyepl, Chapter 28 — Unification is structural equation solving.
(pair(X, f(Y)) = pair(g(a), f(b))).