cf https://github.com/rocq-prover/rocq/pull/21180#issuecomment-3386079677
cf rocq-prover/rocq#21180 (comment)