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