Is the essential similarity of the key trick in Godel's incompleteness theorem and the Y combinator well known? I finally "got" the incompleteness theorem when

Is the essential similarity of the key trick in Godel's incompleteness theorem and the Y combinator well known? I finally "got" the incompleteness theorem when that relationship dawned on me. As a cute entry point, consider the standard lambda term with no normal form, "(lambda x. (x x)) (lambda x. (x x))". Now consider the Godel formula "Substitute(F, n)", which takes a number F, the Godel number of a formula with a single free variable, and another number n. It simplifies to a number M which is the Godel number of the formula F with n replacing all instances of its free variable. One might interpret F as function-like, in the sense that for any number n, F [free_var := n] simplifies to some other number m. So now consider "Substitute(F, F)", which is suggestive of "(x x)" in lambda notation. Let M be the Godel number of this formula, which has one free variable. Finally, use an analogy to the above self-referential lambda term to create the formula G, defined as "Substitute(M, M)". To what number does this arithmetic formula with no free variables simplify? The delightful answer is that it simplifies to its own Godel number! Just as it is a short step from the above simple self-referential lambda term to the Y combinator, so it is a short step from the above fact to the standard Godel formula for which neither it nor its negation has a proof.