MetaRocq.Translations.param_generous_packed is unimportable #1235
Description
Require MetaRocq.Translations.param_generous_packed gives
Error: Universe inconsistency. Cannot enforce MiniHoTT_paths.sigT.u1 <=
MiniHoTT_paths.sigT.u0 because MiniHoTT_paths.sigT.u0
< MiniHoTT_paths.sigT.u1.
Is this deliberate?