ch:capture-types: ch:capture-types

The first substitution gives $\{a,b,y\}$, and removing $y$ gives $\{a,b\}$. The equation $\star [C/x]=\star$ gives $\star [\{a\}/x]=\star$.

By SC-Var, it suffices to derive $\{p\}{\preccurlyeq }_{\mathsf{cap}}\varnothing$. A second SC-Var reduces this to $\varnothing {\preccurlyeq }_{\mathsf{cap}}\varnothing$, the empty instance of SC-Set-L. The declaration of $q$ permits any value capturing at most $p$; neither SC-Var step asserts equality with the declared bound.

Rule App-C substitutes $\mathrm{cv}(\varnothing ▹U_g,\mathrm{\Gamma })=\varnothing$ for $f$. Therefore the result is $\varnothing ▹\mathrm{\Pi }(z:\varnothing ▹\mathrm{\top }).\star ▹\mathrm{\top }$. Capture-set substitution removes $f$ from the singleton; App-C is the typing rule that requests the substitution.

Put $A=\mathrm{\Pi }(z:S).T$ and $F=\star ▹A$. The requested introduction steps are $$\frac{f:F\in \mathrm{\Gamma },f:F}{\mathrm{\Gamma },f:F⊢f:\{f\}▹A}\mathrm{Var}-\mathrm{C}$$ and $$\frac{\mathrm{\Gamma },f:F⊢f:\{f\}▹A}{\mathrm{\Gamma }⊢\lambda (f:F).f:\varnothing ▹\mathrm{\Pi }(f:F).\{f\}▹A}\mathrm{Abs}-\mathrm{C}$$ For $g:\{c,d\}▹A$, the elimination is $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢\lambda (f:F).f:\varnothing ▹\mathrm{\Pi }(f:F).\{f\}▹A\\ \mathrm{\Gamma }⊢g:\{c,d\}▹A\end{array}}{\mathrm{\Gamma }⊢(\lambda (f:F).f)g:\{c,d\}▹A}\mathrm{App}-\mathrm{C}$$

Static widening gives the result domain $\star ▹U$. Exact beta substitution gives $\varnothing ▹U$. Preservation would need . Arrow subtyping reverses domains, so its premise is , which would require $\star {\preccurlyeq }_{\mathsf{cap}}\varnothing$. No subcapturing rule derives that judgment.

If $k\in \mathrm{fv}(v)$, SC-Set-R gives $\{k\}{\preccurlyeq }_{\mathsf{cap}}\mathrm{fv}(v)$. Capture prediction gives $\mathrm{fv}(v){\preccurlyeq }_{\mathsf{cap}}\mathrm{cv}(T,\mathrm{\Gamma })$. Transitivity derives the judgment forbidden by the delimiter. Hence no accepted returned value contains $k$ free.