Implemented unify and polyunify.
Corrected free variables detection.
Now use lists in constructor SForall.