- Keep all <= constraints during refinement, otherwise we might miss collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.