Church pair ($\mathsf{Pair}=\lambda abp.pab$)

With the Church Booleans $\mathsf{T}=\lambda ab.a$ and $\mathsf{F}=\lambda ab.b$, encode a pair byThen $\mathsf{Fst}(\mathsf{Pair}AB){\to }_{\beta }^{\ast }A$ and the second projection similarly returns $B$. Pairing an iteration counter with a computed value implements primitive recursion using only Church numeral iteration.