Fix bug #3559, ensuring a canonical order of universe level quantifications when
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.