Self-quoting fixed point
= Self-quoting fixed point
Let $A$ code application and $C$ code numeral quotation. For a <lambda term> $F$, choose a fresh $x$ and put $H=\lambda x.F(Ax(Cx))$ and $Q=H d(H)$. Then $A d(H)(C d(H))\equiv_\beta d(Q)$, so $Q\equiv_\beta Fd(Q)$. This <diagonal argument> uses the syntax of the actual term $Q$, including any free variables, not an equivalence-class code.