As is standard in models of dependent type theories [1]},
welldefinedness of the interpretation function must be proved by induction on the
structure of derivations, simultaneously with soundness and a substitution lemma,
that we now describe.
<FIGURE>