sketch of a general substitute function.

- This interface isn't quite powerful to unify everything.
  In particular, it needs to communicate that the "none"
  results in exactly the unification variable.