McCarthy’s method depended upon a particular property of recursive functions: the function you could compute using the equations was the smallest (fewest input-output pairs) function that satisfied the equations. Intuitively, this makes sense since any function for which the equations are true, must at least have those pairs. But intuition rarely satisfies mathematicians. Proving the method worked for the λ-calculus came down to proving that the method it used to create recursive functions, the Y combinator, produced the smallest one.
This involved a very complex argument about λ-calculus expressions drawing upon the work of other logicians.
To make a long, painful story short: I proved that the function Yh, where Y is described in the earlier section on the λ-calculus, is the smallest function, f, for which f = hf. Smallest here means replacing Yh imbedded in any larger expression by f will result in a normal form at least as often as the original expression.
Explaining this section properly took 56 out of the 131 pages in my dissertation! The proof of this theorem was so dense that Wozencraft gave up studying it and admitted I had proved an original, difficult theorem.