Based on an idea and WIP commits of J-H. Jourdan: the core of a CMRA
A is now a partial function A → option A.

TODO: define sum CMRA
TODO: remove one shot CMRA and define it in terms of sum

- Make the carrier argument of the constructors for the canonical structures
  cofeT and cmraT explicit. This way we make sure the carrier is properly
  exposed, instead of some alias of the carrier.
- Make derived constructions (such as discreteC and discreteR) notations
  instead of definitions. This is yet again to make sure that the carrier is
  properly exposed.
- Turn DRA into a canonical structure (it used to be a type class).

This fixes some issues, notably it fixes some broken rewrites in algebra/sts
and it makes canonical structures work properly with dec_agree.

The only drawback is that we have to restrict iprod to finite types,
but that is fine.

Thanks to Amin Timany for the suggestion.

Most notably, there is no need to internalize stuff into the logic
as it follows from generic lemmas for discrete COFEs/CMRAs.

This better seals off their definition. Although it did not give
much of a speedup, I think it is conceptually nicer.