Testcase for stdpp!123.
I discovered this bug while fixing a regression in lambdarust/weak.
The lambdarust problem is also related to https://github.com/coq/coq/issues/11799, but the current testcase really needs the more relaxed modes for TCEq
, even if the aforementioned Coq bug is fixed.
This MR needs stdpp!123 (merged)