Mirroring so that we can have it on our boards https://github.com/rocq-prover/rocq/pull/22118
Mirroring so that we can have it on our boards
rocq-prover#22118