Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type.
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.