Bug fix for disequations

Correctly eliminate dqs where the lhs is a parameter.
(Eliminate them if there is only one for a given parameter,
otherwise keep them.)

Also, add path compression for lvar lookup.
Disunification bug fix.

After parameter elimination, check the results to
make sure some pre-existing equality hasn't been
reproduced.