(λx.x(λxy.x))(λx.x(λxy.y))(λx.x) → (λx.x(λxy.y))(λxy.x)(λx.x) → (λxy.x)(λxy.y)(λx.x) → (λy.(λxy.y))(λx.x) → λxy.y
(λy.y((λa.xa)(λa.a)))(λb.b) → (λb.b)((λa.xa)(λa.a)) → (λa.xa)(λa.a) → x(λa.a)