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.
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.