Theorem 2.1.15 (Fixed Point Theorem). There is a λ-term Y such that, for all F:

F(YF)βYF.