finished unify method, needs more testing, check occursIn definition with Prof.