Is it possible to find a lambda term $s$ such that for all terms $t$ and $u$ (of untyped lambda calculus) , $s(tu) = u $ where the equality refers to $\beta$-equality?
I thought that no such $s$ should exist since I don't see how any beta reduction rules would allow us to peel away the brackets so to speak.
Suppose that such a thing existed. Then if we pick:
$$t = λx. λy. y$$
We have:
$$t\ u =_β λ y. y$$
for all $u$. This would mean that:
$$s\ (λ y. y) =_β u$$
for all $u$. However, there are many (β) distinct lambda terms $u$, so this is impossible.