- Better substitution of algebraics in algebraics (for universe variables that
can be algebraics).
- Fix issue #2, Context was not properly normalizing the universe context.
- Fix issue with typeclasses that were not catching UniverseInconsistencies
raised by unification, resulting in early failure of proof-search.
- Let the result type of definitional classes be an algebraic.