\,.\,
{\ensuremath{\mathrm{Cond}\,({\ensuremath{\mathfrak{0}}}x)\,0\,(d_{2,1}^{\ensuremath{\mathrm{Nat}}}x)\,}}$ (predecessor). The rules $i_i^{\ensuremath{\mathrm{Nat}}}$ and $i_t^{{\ensuremath{\mathrm{Nat}}},k}$ become:

[lr]{}\
$
  {n_t^1:}\; \inferrule{
  }{
    \Gamma {\ensuremath{\vdash}}0 : {\ensuremath{\mathrm{Nat}}}}
$ & $
  {n_t^2:}\; \inferrule{
    \Gamma {\ensuremath{\vdash}}t : {\ensuremath{\mathrm{Nat}}}}{
    \Gamma {\ensuremath{\vdash}}({\ensuremath{\mathfrak{s}}}t) : {\ensuremath{\mathrm{Nat}}}}
$

To simplify the exposition, we discuss some properties of our formulation of inductive types using the example of natural numbers. Much of what we say applies to other basic inductive types, with appropriate modifications.

The rule $n_i$ is an induction principle for natural numbers. An important property of this induction principle is that it places no restrictions on $t$. This allows us to prove by induction on natural numbers properties of terms about which nothing is known beforehand. In particular, we do not need to know whether $t$ has a $\beta$-normal form in order to apply the rule $n_i$ to it. In contrast, an induction principle of the form e.g. $$n_i':\;\; \forall f : {\ensuremath{\mathrm{Nat}}}\to {\ensuremath{\mathrm{Prop}}}\,.\, \left(\left(f 0 \wedge (\forall
x : {\ensuremath{\mathrm{Nat}}}\,.\, f x \supset f ({\ensuremath{\mathfrak{s}}}x))\right) \supset \forall x : {\ensuremath{\mathrm{Nat}}}\,.\, f
x\right)$$ would be much less useful, because to apply it to a term $t$ we would have to prove $t : {\ensuremath{\mathrm{Nat}}}\to {\ensuremath{\mathrm{Prop}}}$ *beforehand*. Examples of the use of the rule $n_i$ for reasoning 