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

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