I know that I can $(\lambda x.1) 0 \rhd_\beta 1$. This is the constant 1, but can I contract it automatically? I mean, is $1$ the normal form of $(\lambda x.1)$?
It seems reasonable to do it but when goes to combinators this sense stops, I mean, if I can $\lambda x.1 \rhd_\beta 1$, then I would $\lambda xy.y \rhd_\beta \lambda y.y$ but $(\lambda xy.y) a b \rhd_\beta b$ and $(\lambda x.1) a b \rhd_\beta 1 b$ so that $\lambda x.1 \not\equiv_\beta 1$
What rules I'm missing on Lambda cauculus that forbids the contraction $\lambda x.1 \rhd_\beta 1$?