HO unification, continuing
Slightly better parser: application is left-linear, -> is a notation (no * though).

Finished "stupid" HO unification, which does the same as first order unification.