Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512

This MR provides an alternative to !165 (closed), but avoids the epose horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.

added 1 commit

• 6af69af1 - Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512.

Compare with previous version

mentioned in merge request !165 (closed)

mentioned in commit 2f5854bd

merged