y : {\ensuremath{\mathrm{Nat}}}\,.\, (x < y) : {\ensuremath{\mathrm{Prop}}}$.

\[lem\_le\_eq\] ${\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s} \forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, (x \ge y) \wedge (x \le y)
  \supset (x =_{\ensuremath{\mathrm{Nat}}}y)$.

It is possible to derive Peano axioms for $+$ and ${\ensuremath{\cdot}}$ defined as above.

\[thm\_peano\] The following terms are derivable in the system ${\ensuremath{{\cal I}}}_s$:

-   $\forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, \left({\ensuremath{\mathfrak{s}}}x =_{\ensuremath{\mathrm{Nat}}}{\ensuremath{\mathfrak{s}}}y\right)
        \supset \left(x =_{\ensuremath{\mathrm{Nat}}}y\right)$,

-   $\forall x : {\ensuremath{\mathrm{Nat}}}\,.\, \neg ({\ensuremath{\mathfrak{s}}}x =_{\ensuremath{\mathrm{Nat}}}0)$,

-   $\forall x : {\ensuremath{\mathrm{Nat}}}\,.\, (x + 0 =_{\ensuremath{\mathrm{Nat}}}x)$,

-   $\forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, (x + {\ensuremath{\mathfrak{s}}}y =_{\ensuremath{\mathrm{Nat}}}{\ensuremath{\mathfrak{s}}}(x + y))$,

-   $\forall x : {\ensuremath{\mathrm{Nat}}}\,.\, (x {\ensuremath{\cdot}}0 =_{\ensuremath{\mathrm{Nat}}}0)$,

-   $\forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, (x {\ensuremath{\cdot}}({\ensuremath{\mathfrak{s}}}y) =_{\ensuremath{\mathrm{Nat}}}(x {\ensuremath{\cdot}}y)
        + x)$.

The following theorem shows that any function for which there exists a measure on its arguments, which may be shown to decrease with every recursive call in each of a finite number of exhaustive cases, is typable in our system.

Suppose $\Gamma {\ensuremath{\vdash}}\forall x_1 : \alpha_1 \ldots \forall x_n :
  \alpha_n \,.\, \varphi_1 \lor \ldots \lor \varphi_m$, $\Gamma
  {\ensuremath{\vdash}}\alpha_j : {\ensuremath{\mathrm{Type}}}$ for $j = 1,\ldots,n$, and for $i=1,\ldots,m$: $\Gamma {\ensuremath{\vdash}}\forall x_1 : \alpha_1 \ldots
  \forall x_n : \alpha_n \,.\, t_i : \beta \to \ldots \to \beta$ where $\beta$ occurs 