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.
Showing
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.
mentioned in commit f66f7f16
·mentioned in commit f66f7f16