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 notequiv_beta 1$
What rules I’m missing on Lambda cauculus that forbids the contraction $lambda x.1 rhd_beta 1$?