is no a priori syntactic distinction between terms, formulas, types, type assertions, etc. Formally, there are only terms, but some terms are intuitively interpreted as formulas, types, etc. In particular, the aforementioned method of defining terms by arbitrary recursive equations may be applied to define terms which could be intuitively considered to be formulas, e.g. we may define a term $\varphi$ such that $\varphi =
\neg \varphi$. Inconsistency is avoided, because it will not be actually possible to prove ${\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s} \varphi : {\ensuremath{\mathrm{Prop}}}$, hence $\varphi$ will not really be a formula. In ${\ensuremath{{\cal I}}}_s$ the inference rules serve the purpose of classifying terms into different categories. This classification is not enforced a priori, but instead it is a part of derivations in the logic.

In ${\ensuremath{{\cal I}}}_s$ there is no rule for typing the equality $\mathrm{Eq}$. One consequence is that ${\ensuremath{\vdash}}\neg({\ensuremath{\mathrm{Eq}\,t_1\,t_2\,}})$ cannot be derived for any terms $t_1,t_2$.[^4] For this reason $\mathrm{Eq}$ is more like a meta-level notion of equality.

Leibniz equality $\mathrm{Eql}$ is defined as: $$\mathrm{Eql} \equiv \lambda \alpha \lambda x \lambda y . \forall p :
  \alpha \to {\ensuremath{\mathrm{Prop}}}\,.\, p x \supset p y$$

As with $=$, we will often write $t_1 =_\alpha t_2$ to denote ${\ensuremath{\vdash}}{\ensuremath{\mathrm{Eql}\,\alpha\,t_1\,t_2\,}}$ 