((λa.(xa))(λb.(bx)))[λx.(w(xy))/x]
≡ (λa.((λx.(w(xy)))a))(λb.(b (λx.(w(xy)))))
→ (λx.(w(xy)))(λb.(b(λx.(w(xy)))))
→ (w((λb.(b(λx.(w(xy)))))y))
→ (w(y(λx.(w(xy)))))