Following Hofmann [1]} we define an annotated syntax of pre-terms, pre-types and pre-contexts
(allowing also judgements with no derivations), define an interpretation of this into the model
as a partial function by structural induction, and finally prove that the interpretation of judgements
with derivations are well-defined.
<FIGURE>