The only instance of Core (other than the default one) is for the STS. That does not seem worth it. But trying to get rid of Core leads to all sorts of annoyances in particular around the constructors for (CM)RAs with a unit: I thought we should also change the (cm)ra_total constructors to ask for showing pcore non-expansive instead of core as it seemed more reasonable to ask for a proof of what the user actually wanted. However, that fails miserably; now "by eauto" does not solve these goals any more. Debugging showed that different instances get used for the metric/equiv of option, and that's about as far as I got.
@robbertkrebbers I'd appreciate if you can take a look (but this is very non-urgent).