"\x. (E1 \y. (E2 (E3 E4)))" is the equivalent lambda expression

False. The scope of the abstractions are maximized, but the applications have been associated to the right (they should be to the left.