- Fix handling of polymorphic inductive elimination schemes.
- Avoid generation of dummy universes for unsafe_global*
- Handle side effects better for polymorphic definitions.