Simply type lambda calculus and simple type theory are not equivalent. The former only has rules for alpha- and beta-reduction, the latter also has rules for Modus Ponens, extensionality and the Introduction of the quantification constant $\Pi$. The normalization results for lambda calculus only refer to rewriting modulo alpha- and beta reduction (there are also variants including eta, an extensionality rule for lambda terms).

What is a little confusing is that lambda calculus can encode proofs in simple type theory. This is usually done via the Curry-Howard isomorphism but Farmer uses a different encoding. In both cases, we can verify a proof term by normalization but we can not find these terms by reduction.