Lambda definition of primitive recursion by pair iteration

If total functions $g$ and $h$ are represented by lambda terms $G,H$, defineandAfter $j$ iterations the Church pair holds $(c_j,c_{f(\mathbf{x},j)})$, proved by mathematical induction using the defining recursion equations. Consequently $R$ represents the total primitive recursive function $f$. This statement concerns total inputs and total recursion constituents; it is not an unguarded composition theorem for arbitrary partial functions.