Let $\mathcal{J}_1, \ldots, J_n$ be judgements such that, listed in this order, they form a derivation. Let
$$ \mathcal{J}_n \; \equiv \; \Delta_n \; ; \; \Gamma_n \; \vdash \; M_n \; : \; N_n \; \mid \; J_n $$
be the final judgement in this derivation, with $J_n$ its justification in $λD_0$.
Assume that for all $i < j$: if $\mathcal{J}_i \equiv \Delta_i ; \Gamma_i \vdash M_i : N_i$, then we have that $\Delta_i \; ; \; \Gamma_i \; \vdash \; *: \Box$.
(a) Let $J_n$ be a case of the (weak)-rule. Prove that
$$\Delta_n \; ; \; \Gamma_n \; \vdash \; *: \Box$$
(b) The same if $J_n$ is a case of the (var)-rule.
(c) The same if $J_n$ is a case of the (def)-rule.
(d) The same if $J_n$ is a case of one of the other $λD_0$-rules as given in Figure 9.3.
(a) If $J_n$ is the (weak) rule then it must be the case that
$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash M_n:N_n \quad \Delta_n; \Gamma_n^{\prime} \vdash C:s}{\Delta_n ; \Gamma_n \vdash M_n:N_n} \quad \text{ where } x \notin \Gamma_n^{\prime} $$
where $\Gamma_n \equiv \Gamma_n^{\prime}, x:C$, and $s=*$ or $s=\Box$.
The first premise $\Delta_n ; \Gamma_n^{\prime} \vdash M_n:N_n$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box$.
Using the (weak) rule
$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box \quad \Delta_n; \Gamma_n^{\prime} \vdash C:s}{\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ where } x \notin \Gamma_n^{\prime} $$
This is the conclusion we desire.
(b) If $J_n$ is the (var) rule then it must be the case that
$$ (\textit{var}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash N_n:s}{\Delta_n ; \Gamma_n \vdash M_n:N_n} $$
where $\Gamma_n \equiv \Gamma_n^{\prime}, M_n:N_n$, and $s=*$ or $s=\Box$.
The premise $\Delta_n ; \Gamma_n^{\prime} \vdash N_n:s$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box$.
Using the (weak) rule
$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box \quad \Delta_n; \Gamma_n^{\prime} \vdash N_n:s}{\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ where } x \notin \Gamma_n^{\prime} $$
This is the conclusion we desire.
(c) If $J_n$ is the (def) rule then it must be the case that
$$ (\textit{def}) \quad \frac{\Delta_n^{\prime};\Gamma_n \vdash M_n:M_n \quad \Delta_n^{\prime} ; \bar{x}:\bar{A} \vdash C:D} {\Delta_n ; \Gamma_n \vdash M_n:N_n} \quad \text{ if } a \notin \Delta $$
where $\Delta_n \equiv \Delta_n^{\prime},\bar{x}:\bar{A} \triangleright a(\bar{x}) := C:D$.
The first premise $\Delta_n^{\prime};\Gamma_n \vdash M_n:M_n$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n^{\prime};\Gamma_n \vdash *:\Box$.
Using the (def) rule
$$ (\textit{def}) \quad \frac{\Delta_n^{\prime};\Gamma_n \vdash *:\Box \quad \Delta_n^{\prime} ; \bar{x}:\bar{A} \vdash C:D} {\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ if } a \notin \Delta $$
This is the conclusion we desire.
Note: This exercise is suggesting that correctness is preserved by the $\lambda D_0$ derivation rules.
(d) As an edge case, we'll try the (sort) rule.
If $J_n$ is the (sort) rule then it must be the case that
$$ (\textit{sort}) \quad \emptyset ; \emptyset \vdash *:\Box $$
This is the desired conclusion, with $\Delta = \emptyset, \Gamma = \emptyset$.
