\,.\, \top}
            {\Gamma {\ensuremath{\vdash}}(\epsilon \alpha) : \alpha}
          $ & $
            {p_i:}\; \inferrule{\Gamma {\ensuremath{\vdash}}\varphi}
            {\Gamma {\ensuremath{\vdash}}\varphi : {\ensuremath{\mathrm{Prop}}}}
          $\
    &\
    $
          {c_1:}\; \inferrule{
            \Gamma {\ensuremath{\vdash}}\varphi
          }{
            \Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,({\ensuremath{\mathrm{Cond}\,\varphi\,t_1\,t_2\,}})\,t_1\,}}
          }
          $ & $
          {c_2:}\; \inferrule{
            \Gamma {\ensuremath{\vdash}}\neg\varphi
          }{
            \Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,({\ensuremath{\mathrm{Cond}\,\varphi\,t_1\,t_2\,}})\,t_2\,}}
          }
          $\
    &\
    \
    &\
    \
    &\
    \
    &\
    $
            {\mbox{eq}:}\; \inferrule{\Gamma {\ensuremath{\vdash}}\varphi \\ \Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,\varphi\,\varphi'\,}}}{\Gamma {\ensuremath{\vdash}}\varphi'}
          $ & $
          {\mbox{eq-sym}:}\; \inferrule{\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,t_1\,t_2\,}}}{\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,t_2\,t_1\,}}}
          $\
    &\
    \
    &\
    \
    &\

    $${i_i^\iota:}\; \inferrule{\Gamma, x_1 : \iota_{i,1}^*, \ldots, x_{n_i} : \iota_{i,n_i}^*, t
              x_{j_{i,1}}, \ldots, t x_{j_{i,k_i}} {\ensuremath{\vdash}}t (c_i^\iota x_1 \ldots
              x_{n_i}) \\ \mathrm{for\ } i=1,\ldots,m
            }{
              \Gamma {\ensuremath{\vdash}}\forall x : \iota \,.\, t x
            }$$ where $x,x_1,\ldots,x_{n_i} \notin FV(\Gamma, t)$, $c_1^\iota,\ldots,c_m^\iota \in {\ensuremath{{\cal C}}}$ are all constructors associated with $\iota \in {\ensuremath{{\cal T}}}_I$, and $j_{i,1},\ldots,j_{i,k_i}$ is an increasing sequence of all indices $1 \le j \le n_i$ such that $\iota_{i,j} = \star$ $${i_t^{\iota,k}:}\; \inferrule{
              \Gamma {\ensuremath{\vdash}}t_j : \iota_{k,j}^* \mathrm{\ for\ } j=1,\ldots,n_k
            }{
              \Gamma {\ensuremath{\vdash}}(c_k^\iota t_1 \ldots t_{n_k}) : \iota
            }$$

For an arbitrary set of terms $\Gamma$, we write $\Gamma
  {\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s} \varphi$ if there exists a finite subset $\Gamma'
  \subseteq \Gamma$ such that $\Gamma' {\ensuremath{\vdash}}\varphi$ is derivable in the system ${\ensuremath{{\cal I}}}_s$. We drop the subscript when irrelevant or obvious from the 