Library MetaCoq.Translations.param_cheap_packed_correctness