-
Jacques-Henri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.
866cad62
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.