Unification

I'm reading a Haskell tutorial:
http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm

where is the proof that unification always exists?

>>3
fixed point function is useless?

Also I noticed that these  (* comments *) would be ideal for Lisp, instead of #| ugliness |#. Although ($ would be better $) because of * being reserved for multiplication.

i.e. instead of #|(if A B C)|# it could have been commented as ($if A B C$)