repair unsoundness problem in translation of unknown expressions

Previous routine translated e.g. `f(x) == f(y)` to `undefined ==
undefined`, which is obviously unsound. Now, it registers fresh
variables for each unknown subterm.