# How does one show $(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$ in lambda calculus?

I wanted to show:

$$(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$$

the definition of beta equivalence is on page 17 of these notes.

I did a few attempts but got different things like $$x$$. I think my main confusion is how to interpret:

$$yx$$

at the end. Does that mean we are applying $$x$$ to $$y$$ or that we are applying $$yx$$ to the lambda function $$(\lambda x . (\lambda y.x))$$? I tried both interpretations and didn't get anything that made sense.

I think I understand what $$\beta$$ conversion means (cuz I could follow the example he gave) but then when I tried doing it myself on this weird example I got non-sense.

I will make my answer more sophisticated by using parentheses. The first thing to realize is that $$(\lambda x . (\lambda y . x)) y x$$ is the same thing as $$((\lambda x . (\lambda y . x)) y) x$$ because in $$\lambda$$-calculus application associates to the left, which means that $$A B C = (A B) C$$. As you can see, $$x y$$ does not even appear in your expression.
After that, I would follow Yuval's observation that it is impolite to use the same variable for two different purposes: the $$x$$ and $$y$$ inside $$\lambda$$'s are not the same as the outer $$x$$ and $$y$$. We should rename bound variables to get $$((\lambda a . (\lambda b . a)) y) x$$ Can you do it from here?
P.S. Please stop pelting us with questions about $$\lambda$$-calculus that all look alike. Take them one at a time, wait for the answers, and think about them. It is likely subsequent questions will become redundant.
Let's change the leftmost $$y$$ to a $$z$$, to avoid confusion.
When you apply $$\lambda x. (\lambda z.x)$$ to $$y$$, you get $$\lambda z.y$$. When you apply this to $$x$$ (indeed, to anything at all), you get $$y$$.