Although this proof, it can be found in [1], is subject to the constraints that Goedel's 2nd theorem enforces: the proof uses a stronger logic that HOL itself.

Although this proof, it can be found in [1], is subject to the constraints that Goedel's 2nd theorem enforces: the proof uses a stronger logic that HOL itself. In this case it uses a large cardinal axiom. [1] J. Harrison, Towards self-verification of HOL Light. https://www.cl.cam.ac.uk/~jrh13/papers/holhol.html https://www.cl.cam.ac.uk/~jrh13/papers/holhol.html