In Section 7, the extensionality is written incorrectly as [all x all y all z] (xy)=(zy) -> x=z. It should be [all x all z] ([all y] (xy)=(zy)) -> x=z. The clause form of extensionality (clause 4) should be s(x,g(x,z)) != s(z,g(x,z)) | x=z, and clauses 6 and 7 should have the Skolem term g(J,K). Otherwise, the proof is correct.
Section 2.4, Problem 4. The example S (S (K S) K) (S (K (S (S (S K K) (S K K)))) K) of a U combinator is incorrect. We switched the variables when constructing the combinator: in fact, it behaves like a combinator U', where U'xy = x(yyx).
Page 164, 6 lines from the bottom of the page. The equation for collapsing a pair of absorption equations should be p(u,g(x),x) = p(u,h(y),y).
Please let me know if you find any substantial errors not listed here.