Section  defines the interpretation of syntax into the model and proves soundness. For this we
follow the approach of Hofmann [1]} for modelling dependent type theories: First the interpretation
of syntax is defined as a partial function, then it is proved that the interpretation is defined for all judgements that have
a derivation. The latter proof is done by a simultaneous induction with proofs of soundness and a substitution lemma.
As is standard, the syntax interpreted into the model is an annotated variant of the syntax presented in Section .
Apart from the standard annotations e.g. of application terms with the \(\Pi \) -type of the function, in CloTT the term
for application to the tick constant \(\diamond \)  must be changed by replacing a substitution by an explicit substitution. Moreover,
special lemmas for weakening substitutions must be proved to accommodate tick-weakening in CloTT. The paper ends
with conclusions and future work in Section .
