Add the examples on unification and on finding principal solution.
Add the constraint set derivation for (lambda (x) (x x))