Refactor bigops

Currently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick one operator to be used in bigops, whereas we may also want to use big conjunction.

Instead we should do sth. like ssreflect does, with a typeclass/canonical structure for this special purpose that's completely separate from the main algebraic hierarchy.