Unification now may perform parallel beta-reduction, and the instantiation tactic was tweaked. I still doubt its completeness, but it handles more cases. Corrected some spelling errors in the comments.