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.