context.

If $\Gamma {\ensuremath{\vdash}}\varphi$ then $\Gamma, \psi {\ensuremath{\vdash}}\varphi$.

\[lem\_I\_s\_subst\] If $\Gamma {\ensuremath{\vdash}}\varphi$ then $\Gamma[x/t] {\ensuremath{\vdash}}\varphi[x/t]$, where $\Gamma[x/t] = \{ \psi[x/t] \;|\; \psi \in \Gamma \}$.

Representing Logic
------------------

The inference rules of ${\ensuremath{{\cal I}}}_s$ may be intuitively justified by appealing to an informal many-valued semantics. A term $t$ may be true, false, or something entirely different (“undefined”, a program, a natural number, a type, …). By way of an example, we explain an informal meaning of some terms:

-   $t : {\ensuremath{\mathrm{Prop}}}$ is true iff $t$ is true or false,

-   $\alpha : {\ensuremath{\mathrm{Type}}}$ is true iff $\alpha$ is a type,

-   $t : \alpha$ is true iff $t$ has type $\alpha$, assuming $\alpha$ is a type,

-   $\forall x : \alpha . \varphi$ is true iff $\alpha$ is a type and for all $t$ of type $\alpha$, $\varphi[x/t]$ is true,

-   $\forall x : \alpha . \varphi$ is false iff $\alpha$ is a type and there exists $t$ of type $\alpha$ such that $\varphi[x/t]$ is false,

-   $t_1 \vee t_2$ is true iff $t_1$ is true or $t_2$ is true,

-   $t_1 \vee t_2$ is false iff $t_1$ is false and $t_2$ is false,

-   $t_1 \supset t_2$ is 