------------------------------------------------------------------------------ ----------------------------------------------------------------------------------------------------------------------------------------

Equality, Recursive Definitions and Extensionality
--------------------------------------------------

It is well-known (see e.g. [@Barendregt1984 Chapters 2, 6]) that since untyped $\lambda$-terms are available together with the axiom $\beta$ and usual rules for equality, any set of equations of the following form has a solution for $z_1,\ldots,z_n$, where the expressions $\Phi_i(z_1, \ldots, z_n, x_1, \ldots, x_m)$ are arbitrary terms with the free variables listed. $$\begin{aligned}
  z_1 x_1 \ldots x_m &=& \Phi_1(z_1, \ldots, z_n, x_1, \ldots, x_m) \\
  &\vdots& \\
  z_n x_1 \ldots x_m &=& \Phi_n(z_1, \ldots, z_n, x_1, \ldots, x_m)\end{aligned}$$ In other words, for any such set of equations, there exist terms $t_1,
\ldots, t_n$ such that for any terms $s_1, \ldots, s_m$ we have ${\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,\left(t_i s_1 \ldots s_m\right)\,\left(\Phi_i(t_1,
  \ldots, t_n, s_1, \ldots, s_m)\right)\,}}$ for each $i=1,\ldots,n$.

We will often define terms by such equations. In what follows we freely use the notation $t_1 = t_2$ for ${\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,t_1\,t_2\,}}$, or for $\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,t_1\,t_2\,}}$ when it is clear which context $\Gamma$ is meant. We use $t_1 = t_2 = \ldots = t_n$ to indicate that ${\ensuremath{\mathrm{Eq}\,t_i\,t_{i+1}\,}}$ may be derived for $i=1,\ldots,n-1$. We also sometimes write a term of the form ${\ensuremath{\mathrm{Eq}\,t_1\,t_2\,}}$ as $t_1 = t_2$.

It is worth stressing once again that there 