for $k=1,\ldots,n_i$, if $c_i^\iota \in {\ensuremath{{\cal C}}}$ has arity $n_i$

    -   $\Gamma {\ensuremath{\vdash}}\bot : {\ensuremath{\mathrm{Prop}}}$

    -   $\Gamma {\ensuremath{\vdash}}\forall p : {\ensuremath{\mathrm{Prop}}}\,.\, p \lor \neg p$

    -   $\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,((\lambda x \,.\, t_1)
              t_2)\,(t_1[x/t_2])\,}}$

    [**Rules**]{}

    [cc]{}\
    &\
    \
    &\
    \
    &\
    \
    &\
    \
    &\
    $
          {\vee_{i1}:}\; \inferrule{\Gamma {\ensuremath{\vdash}}\varphi}
          {\Gamma {\ensuremath{\vdash}}\varphi \vee \psi}
          $ & $
          {\vee_{i2}:}\; \inferrule{\Gamma {\ensuremath{\vdash}}\psi}
          {\Gamma {\ensuremath{\vdash}}\varphi \vee \psi}
          $\
    &\
    \
    &\
    \
    &\
    $
            {\wedge_{e1}:}\;
            \inferrule{
              \Gamma {\ensuremath{\vdash}}\varphi \wedge \psi
            }{
              \Gamma {\ensuremath{\vdash}}\varphi
            }
          $ & $
            {\wedge_{e2}:}\;
            \inferrule{
              \Gamma {\ensuremath{\vdash}}\varphi \wedge \psi
            }{
              \Gamma {\ensuremath{\vdash}}\psi
            }
          $\
    &\
    $
            {\supset_{t2}:}\;
            \inferrule{
              \Gamma {\ensuremath{\vdash}}(\varphi \supset \psi) : {\ensuremath{\mathrm{Prop}}}}{
              \Gamma {\ensuremath{\vdash}}\varphi : {\ensuremath{\mathrm{Prop}}}}
          $ & $
            {\bot_{e}:}\;
            \inferrule{
              \Gamma {\ensuremath{\vdash}}\bot
            }{
              \Gamma {\ensuremath{\vdash}}\varphi
            }
          $\
    &\
    \
    &\
    $
          {\to_e:}\; \inferrule{\Gamma {\ensuremath{\vdash}}t_1 : \alpha \to \beta \\ \Gamma {\ensuremath{\vdash}}t_2 : \alpha}{\Gamma {\ensuremath{\vdash}}t_1
            t_2 : \beta}
          $ & $
            {\to_t:}\; \inferrule{\Gamma {\ensuremath{\vdash}}\alpha : {\ensuremath{\mathrm{Type}}}\\ \Gamma
              {\ensuremath{\vdash}}\beta : {\ensuremath{\mathrm{Type}}}}
            {\Gamma {\ensuremath{\vdash}}(\alpha \to \beta) : {\ensuremath{\mathrm{Type}}}}
          $\
    &\
    \
    &\
    $
            {s_e:}\; \inferrule{\Gamma {\ensuremath{\vdash}}t : \{ x :
              \alpha \;|\; \varphi \}}{\Gamma {\ensuremath{\vdash}}\varphi[x/t]}
          $ & $
            {s_{et}:}\; \inferrule{\Gamma {\ensuremath{\vdash}}t : \{ x :
              \alpha \;|\; \varphi\}}{\Gamma {\ensuremath{\vdash}}t : \alpha}
          $\
    &\
    \
    &\
    $
            {\epsilon_i:}\; \inferrule{\Gamma {\ensuremath{\vdash}}\exists x : \alpha 