or $\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eql}\,\alpha\,t_1\,t_2\,}}$, or write $t_1 =_\alpha t_2$ instead of ${\ensuremath{\mathrm{Eql}\,\alpha\,t_1\,t_2\,}}$.

\[lem\_leibniz\] If $\Gamma {\ensuremath{\vdash}}\alpha : {\ensuremath{\mathrm{Type}}}$ then

-   $\Gamma {\ensuremath{\vdash}}\forall x, y : \alpha \,.\, (x =_\alpha y) : {\ensuremath{\mathrm{Prop}}}$,

-   $\Gamma {\ensuremath{\vdash}}\forall x : \alpha \,.\, (x =_\alpha x)$,

-   $\Gamma {\ensuremath{\vdash}}\forall x, y : \alpha \,.\, (x =_\alpha y) \supset
        (y =_\alpha x)$,

-   $\Gamma {\ensuremath{\vdash}}\forall x, y, z : \alpha \,.\, (x =_\alpha y)
        \wedge (y =_\alpha z) \supset (x =_\alpha z)$.

The system ${\ensuremath{{\cal I}}}_s$, as it is stated, is intensional with respect to Leibniz equality. We could add the rules $$e_f:\;
\inferrule{
  \Gamma {\ensuremath{\vdash}}\alpha : {\ensuremath{\mathrm{Type}}}\\ \Gamma {\ensuremath{\vdash}}\beta : {\ensuremath{\mathrm{Type}}}}{
  \forall f_1, f_2 : \alpha \to \beta \,.\, (\forall x
  : \alpha \,.\, f_1 x =_\beta f_2 x) \supset (f_1 =_{\alpha\to\beta} f_2)
}$$ $$e_b:\;
\inferrule{
  \Gamma {\ensuremath{\vdash}}\varphi_1 \supset \varphi_2 \\
  \Gamma {\ensuremath{\vdash}}\varphi_2 \supset \varphi_1
}{
  \Gamma {\ensuremath{\vdash}}\varphi_1 = \varphi_2
}$$ to obtain an extensional variant $e{\ensuremath{{\cal I}}}_s$ of ${\ensuremath{{\cal I}}}_s$. The system $e{\ensuremath{{\cal I}}}_s$ is still consistent – the model we construct for ${\ensuremath{{\cal I}}}_s$ validates the above rules.

${\ensuremath{\vdash}}_{e{\ensuremath{{\cal I}}}_s} \forall x, y : {\ensuremath{\mathrm{Prop}}}\,.\, (x =_{\ensuremath{\mathrm{Prop}}}y) \supset (x
  = y)$

Induction and Natural Numbers {#sec_induction}
-----------------------------

The system ${\ensuremath{{\cal I}}}_s$ incorporates basic 