Significant improvements to unification respecting triggers. Next up: what to do for unification when no UVars occur alone in function terms?