Arithmetical Predicates and Function Quantifiers
S. C. Kleene · Transactions of the American Mathematical Society · 1955
2) The normal form and enumeration theorems for l>0 can be rewritten using a instead of 5, where sW=IIi<.P?m+1 (cf-[7]).Thus in IM pp.291, 292 we have T?(z, a, x) = T\(a(x), z, a, x).Putting t[{w, 0, a) = T[(Y[i)), then T\(a(x), z, a, x) = T\{a{x), z, a).