The generalised continuum hypothesis implies the axiom of choice in Coq. - Dominik Kirst; Felix Rech (CPP, 2021)