진작 볼걸


Let M ≡ λy. N[y] and ￢(x ∈ FV(M)).

Then λx. M x ≡ λx. (λy. N[y]) x = λx. N[x] ≡ λy. N[y] ≡ M.

∴λx. M x = M.