The nicest and clearest presentation of first-order unification I know of is in this book:<p><a href="https:&#x2F;&#x2F;www21.in.tum.de&#x2F;~nipkow&#x2F;TRaAT&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www21.in.tum.de&#x2F;~nipkow&#x2F;TRaAT&#x2F;</a><p>From there it is a simple means to form and solve the type equations needed for Hindley Milner.