 Definition (ordered tuples, natural numbers) The ordered tuple \(\langle a_0,\ldots a_n\rangle\) of \(\lambda\)-terms is defined as \(\lambda x[x a_0\ldots a_n]\).  One then defines the \(\lambda\)-term \(\ulcorner n\urcorner\) corresponding to the natural number \(n\) as: \(\ulcorner 0\urcorner = \mathbf{I}\) and, for every \(k\), \(\ulcorner k + 1\urcorner = \langle \mathbf{F}, \ulcorner k\urcorner\rangle\).