ch:contextual-modal-tt: ch:contextual-modal-tt

The modal lookup and the one-component substitution give $$\frac{u::A[x:A]\in \mathrm{\Delta }\mathrm{\Delta };z:A⊢z/x:x:A}{\mathrm{\Delta };z:A⊢\mathsf{clo}(u,z/x):A}\mathrm{Meta}.$$ Applying Ctx-I yields $\mathrm{\Delta };y:A⊢\mathsf{box}(z:A.\mathsf{clo}(u,z/x)):[z:A⊢A]$. For the altered body, Ctx-I asks for $\mathrm{\Delta };z:A⊢y:A$. Variable lookup fails because its ordinary context contains only $z:A$; the ambient declaration $y:A$ is not a premise of the rule.

Substitution first reaches the neutral head and produces a canonical lambda: $$[\lambda (z:A).z/f{]}_{A^{-}\to A^{-}}f=\lambda (z:A).z.$$ The application clause would therefore create $(\lambda (z:A).z)y$. It does not return that noncanonical redex; it immediately continues with the lambda body at the domain approximation: $$[\lambda (z:A).z/f{]}_{A^{-}\to A^{-}}(fy)=[y/z{]}_{A^{-}}z=y.$$ The term body need not be smaller than the original application, but the outer index has decreased strictly from $A^{-}\to A^{-}$ to its proper subexpression $A^{-}$.

The normal component $M/x$ forbids erasing $x$’s approximation, while the atomic component $R//y$ permits either retaining or erasing $y$’s. The complete list is therefore $$(x:A^{-},y:B^{-})\text{and}(x:A^{-},y:).$$ There are no other choices. Erasing $x$’s type would lose the termination index needed if substituting its normal component creates a redex. The atomic component for $y$ cannot create a head redex, so keeping $B^{-}$ is safe but not required.

At the simply typed layer, let $I=\lambda (x:A).x$ and take $$\mathsf{letbox}(\mathsf{box}(\cdot .I),u.\mathsf{clo}(u,\cdot )).$$ It has type $A\to A$ and its box redex contracts to $I$. If the $\mathsf{letbox}$ occurs in function position, a commuting conversion must first expose that principal redex.

At the canonical layer, assume a closed constant $c:A$ and a meta-variable $$u::(\prod _{v::A[\cdot ]}A)[\cdot ].$$ The atomic term $\mathsf{mapp}(\mathsf{clo}(u,\cdot ),\hat{\cdot }.c)$ synthesizes (A). Hereditarily substitute $\hat{\cdot }.\mathsf{mlam}(v.\mathsf{clo}(v,\cdot ))$ for (u). Substitution into the atomic head returns a meta-abstraction, so the contextual-application clause creates a meta-level beta-redex. It immediately substitutes $\hat{\cdot }.c$ for (v) in $\mathsf{clo}(v,\cdot )$, returning (c) at the strictly smaller domain approximation. Thus the first calculus normalizes an independently defined reduction relation, while the second contracts a newly created redex inside its typing computation. The examples do not transfer strong normalization between the calculi.