# Lambda Calculus: Reduce $(\lambda x. (\lambda y. x \ y) \ x) \ (\lambda z.p)$

According to the answer sheet it is supposed to reduce to $$p$$, but I dont know how. This is what I do

$$(\lambda x. (\lambda y. x \ y) \ x) \ (\lambda z.p)$$

I replace $$x$$ with $$(\lambda z.p)$$

$$\rightarrow (\lambda y. (\lambda z.p) \ y) \ (\lambda z.p))$$

And now $$y$$ with $$(\lambda z.p)$$ to get:

$$\rightarrow (\lambda z.p) \ (\lambda z.p)$$

How do you reduce this to $$p$$? (If it is possible)

In general, $$\beta$$-reduction $$\to_\beta$$ is a binary relation on $$\lambda$$-terms defined as follows: \begin{align} (\lambda z.t)u \to_\beta t\{u/z\} \end{align} where $$t \{u/z\}$$ is the $$\lambda$$-term obtained from $$t$$ by substituting $$u$$ for each free occurrence of $$z$$ in $$t$$.
Now, in your last $$\lambda$$-term $$(\lambda z. p) (\lambda z.p)$$ I guess $$p$$ is either a closed term (i.e. without free variables) or a variable distinct from $$z$$. In both cases, according to the general definition of $$\to_\beta$$: \begin{align} (\lambda z.p) (\lambda z.p) \to_\beta p \{\lambda z.p\ /\,z\} = p. \end{align}
Note that the argument (i.e. the subterm on the right) $$\lambda z.p$$ of the application $$(\lambda z.p)(\lambda z.p)$$ is simply discarded after the $$\beta$$-step, because there are no free occurrences of $$z$$ in $$p$$.
$$(\lambda z. p) \alpha$$ reduces to $$p$$ for any $$\alpha$$.