\supset \psi\rceil}} = {\ensuremath{\lceil\varphi\rceil}} \supset
      {\ensuremath{\lceil\psi\rceil}}$,

-   ${\ensuremath{\lceil\forall x : \tau \,.\, \varphi\rceil}} = \forall x :
      {\ensuremath{\lceil\tau\rceil}} \,.\, {\ensuremath{\lceil\varphi\rceil}}$.

If $\Delta$ is a set of formulas, then ${\ensuremath{\lceil\Delta\rceil}}$ denotes the image of ${\ensuremath{\lceil-\rceil}}$ on $\Delta$. The set $\Gamma(\Delta)$ is defined to contain the following:

-   $x : {\ensuremath{\lceil\tau\rceil}}$ for all $\tau \in {\ensuremath{{\cal T}}}$ and all $x \in
      FV(\Delta)$ such that $x \in V_\tau$,

-   $c : {\ensuremath{\lceil\tau\rceil}}$ for all $\tau \in {\ensuremath{{\cal T}}}$ and all $c \in
      \Sigma_\tau$,

-   $\tau : {\ensuremath{\mathrm{Type}}}$ for all $\tau \in {\ensuremath{{\cal B}}}$,

-   $y : \tau$ for all $\tau \in {\ensuremath{{\cal B}}}$ and some $y \in V_\tau$ such that $y \notin FV(\Delta)$.

The last point is needed because in ordinary logic one always assumes that the domains are non-empty.

\[thm\_sound\_hol\] If $\Delta {\ensuremath{\vdash}}_{\mathrm{CPRED}\omega} \varphi$ then $\Gamma(\Delta, \varphi), {\ensuremath{\lceil\Delta\rceil}} {\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s}
  {\ensuremath{\lceil\varphi\rceil}}$. The same holds if we change CPRED$\omega$ to and ${\ensuremath{{\cal I}}}_s$ to $e{\ensuremath{{\cal I}}}_s$.

The above theorem shows that ${\ensuremath{{\cal I}}}_s$ may be considered an extension of ordinary higher-order logic. This extension is essentially obtained by relaxing typing requirements on allowable $\lambda$-terms. Type-checking is obviously undecidable in ${\ensuremath{{\cal I}}}_s$, but the purpose of types in illative systems is not to have 