The generalised continuum hypothesis implies the axiom of choice in Coq.

Dominik Kirst, Felix Rech

Browse the full CPP paper archive.