 Theorem 4.2 (Gödel 1958) Suppose \(\cD\) is a proof of A in HA and \(A^D\) as in \((\ref{D-Form})\). Then one can effectively construct a sequence of terms \(\vec t\) (from \(\cD\)) such that \({T}\) proves \(A_D(\vec t,\vec y\,)\).