Fix UnifyingResolution

Change from recursive subsitution to non-recursive one is now done.
Clean UnifyingResolution

Used :_* to clean up a 'getVarsFromExpr', which was also renamd.