- Better handling of eta-expansion in unification but still incomplete.
- Remove dead code related to previous implementation of univ polymorphism.