Thanks, in your case the informal definition is clear. I believe in the Quanta article the second and third argument of sub are switched relative to yours.

Another question, do you use Cantor-style diagonalization for the fixed-point theorem? Apparently this is the case for the standard proof of incompleteness, as explained here, though this paper goes over my head: https://haimgaifman.files.wordpress.com/2016/07/22odel-to-kl...

The reason why I'm asking is that Cantor used diagonalization in his famous "diagonal argument" for the real numbers being uncountable. Some people found this argument unconvincing, because it relied on perhaps questionable assumptions, like the decimal representation of real numbers and that different decimal representations must denote a different real number. But if the diagonal argument (or his earlier powerset argument) could be formalized and checked with Coq, doubts would presumably be removed.