Re-do the basics: Cofe's and (CM)RA's

Slim down the algebraic hierarchy to contain only Cofe's, RA's and CMRA's, all as unbundled typeclasses and bundled canonical structures. Instead of a general notion of monotone function, we only really need one functor that maps a CMRA to monotone, step-indexed predicates over that CMRA. Maybe call that uPred? THat's kind of what it is, though it's not the same uPred that we had originally - that one could only deal with RA's.

Then we don't need the notion of a canonical partial order on a type - often, it's not even clear which one that should be. This also gives us the opportunity to define the metric and order on that uPred such that we can have "own(a) => valid(a)" as opposed to right now, where we have "own(a) \vs valid(a)". It's not entirely clear yet though if that latter part will actually work out without significant pain.