From Alexander Williams's "Arguments in Syntax and Semantics" (pp. 213-214):
"Formula (10b) has (9b) and (7b) as provable syntactic consequences, by Conjunction Elimination in the scope of an existential quantifier."
How is (7b) a syntactic consequence of (10b)? Ignoring the $\lambda e_1$ and "$Do(e_1,Floyd)$"for a moment, I believe that we can prove (in first order logic) that $$\exists e_2[Cause(e_1,e_2)\land \exists e_3[Become(e_2,e_3)\land Hard (e_3,glass)]]$$ syntactically entails $$\exists e_3[Hard (e_3,glass)]$$
The author doesn't give any inference rules for lambda calculus, so I don't know how to deal with the lambda. I could guess that the way it works is that we just add $\lambda e_1$ at the beginning of both lines above, and that would be a valid inference, but if so, I still don't see how $\lambda e_1[\exists e_3[Hard(e_3,glass)]]$ syntactically entails $\lambda e_1 [Hard(e_1,glass)].$ Also, I don't see how to eliminate $Do(e_1,Floyd)$.