I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available on the Web.)
The theorem states that a function is $\lambda$2-definable iff it is HG (Herbrand-Goedel) computable and provably type correct in $\lambda$PRED2. The author delegates the proof to a proceeding in FOCS, i.e., Reasoning about functional programs and complexity associated with type disciplines (1983) by Leivant. The corresponding theorem in the proceeding is Theorem 3.1 and Corollary 3.2, although they are stated in terms of provable type-correctness in $\lambda$2, not in $\lambda$PRED2.
The first problem I'm running into is that the definition of HG computability by Barendregt doesn't make sense. IMHO, the equation in Definition 5.4.39.1 should be replaced by $$ \mathit{HG} \vdash p:(f_n(t^\sim) =_L (f(t))^\sim). $$
Assuming this, I tried to prove the equivalent of Theorem 3.1 (Leivant) in terms of $\lambda$PRED2, but in vain. Leivant's proof is informal and I have hard times formalizing it. (By using Barendregt's notation, I'm pretty sure that if $B$ is the proof of $f$'s type correctness then $[B]$ is a $\lambda$2-term that represents $f$, but I am unable to prove this.) Besides, his proof deals with only one direction of the equivalence (provably type correct $\Rightarrow$ $\lambda$2-definable) and the rest is left unstated. I suppose the opposite direction involves the formalization of SN, but I am unsure.
I would be the most grateful for detailed explanation of Theorem 5.4.40.3 by Barendregt.