Find a way to reduce usage of O/R/U suffixes
It is very annoying to have to remember those O/R/U suffices for our algebra instances. This comes up mostly when defining inG
. It would be good to find a way to avoid having to remember and use them.
@robbertkrebbers proposed some scheme similar to the already existing ofe_mixin_of
.