as follows. For each $\iota \in {\ensuremath{{\cal T}}}_I$ of the form $$\iota = \mu(\langle \iota_{1,1},\ldots,\iota_{1,n_1} \rangle,
          \ldots, \langle \iota_{m,1},\ldots,\iota_{m,n_m} \rangle) \in
          {\ensuremath{{\cal T}}}_I$$ where $\iota_{i,j} \in {\ensuremath{{\cal T}}}_I \cup \{\star\}$, the set ${\ensuremath{{\cal C}}}$ contains $m$ distinct constants $c_1^\iota,\ldots,c_m^\iota$. The number $n_i$ is called the *arity* of $c_i^\iota$, and $\langle \iota_{i,1},\ldots,\iota_{i,n_i} \rangle$ is its *signature*. With each $c_i^\iota \in {\ensuremath{{\cal C}}}$ of arity $n_i$ we associate $n_i$ distinct destructors $d_{i,1}^\iota,\ldots,d_{i,n_i}^\iota \in {\ensuremath{{\cal D}}}$ and one test $o_i^\iota \in {\ensuremath{{\cal O}}}$. When we use the symbols $c_i^\iota$, $o_i^\iota$ and $d_{i,j}^\iota$ we implicitly assume that they denote the constructors, tests and destructors associated with $\iota$. When it is clear from the context which type $\iota$ is meant, we use the notation $\iota_{i,j}^*$ for $\iota_{i,j}$ if $\iota_{i,j} \ne \star$, or for $\iota$ if $\iota_{i,j} = \star$.

-   The set of *${\ensuremath{{\cal I}}}_s$-terms* ${\ensuremath{\mathbb T}}$ is defined by the following grammar. $$\begin{aligned}
          {\ensuremath{\mathbb T}}&::=& V_s \;|\; \Sigma_{s} \;|\; {\ensuremath{{\cal S}}}\;|\; {\ensuremath{{\cal C}}}\;|\; {\ensuremath{{\cal D}}}\;|\; {\ensuremath{{\cal O}}}\;|\; {\ensuremath{{\cal T}}}_I \;|\; \lambda V_s \,.\, {\ensuremath{\mathbb T}}\;|\; ({\ensuremath{\mathbb T}}{\ensuremath{\mathbb T}})
          \;|\; \mathrm{Is} \;|\; \mathrm{Subtype} \;|\; \mathrm{Fun}
          \;|\; \\ && \forall \;|\; \vee \;|\; \bot \;|\; \epsilon \;|\;
          \mathrm{Eq} \;|\; \mathrm{Cond}
        \end{aligned}$$ We assume application associates to the 