ch:nominal-syntax: ch:nominal-syntax

Choose $c\notin \{a,b\}$. Since $c\mathrm{\#}\mathsf{var}(a)$, $$[b]\mathsf{var}(a)=[c](bc)\cdot \mathsf{var}(a)=[c]\mathsf{var}(a).$$ This representative is fresh for the substituting term $\mathsf{var}(b)$, so $${\mathsf{lam}}_B([b]\mathsf{var}(a))[\mathsf{var}(b)/a]={\mathsf{lam}}_B([c]\mathsf{var}(b)).$$ Decoding gives $\lambda (c:B).b$, an alpha-variant of every result with a fresh binder. The captured term $\lambda (b:B).b$ has no free $b$ and is not alpha-equivalent to it.

The application body has support $\{a,b\}$ and name abstraction removes its bound $a$, hence $\mathrm{supp}(t)=\{b\}$. Equivariance of least support gives $$\mathrm{supp}((ac)\cdot t)=(ac)\cdot \{b\}=\{b\},$$ because $a,b,c$ are distinct. The transposition $(bc)$ fixes every atom of the empty set but changes the free occurrence of $b$ to $c$; therefore the empty set does not support $t$.

The three least supports are respectively $$\{a\},\{a,b\},\{b\}.$$ For $\mathsf{var}(a)$, the transposition $(ac)$ fixes the empty remainder and changes the term. For the application, $(ac)$ fixes $b$ and changes the left component, while $(bc)$ fixes $a$ and changes the right component. For the abstraction, $(bc)$ changes its sole free atom. Thus every atom in each displayed support is necessary; proposition 62.3 gives minimality.

Let $a,b,c$ be distinct. First take $t=\mathsf{var}(b)$ and $u=\mathsf{var}(c)$. Then $t[u/a]=\mathsf{var}(b)$, so the left support is $\{b\}$, whereas the bound’s right side is $\{b,c\}$.

For a bound occurrence, take $t={\mathsf{lam}}_A([a]\mathsf{var}(a))$ and the same $u$. Substitution renames the binder away from $a,c$ before descending and leaves the bound identity alpha-equivalent to itself. Its support is empty. The right side of the support inclusion is $\varnothing \cup \{c\}=\{c\}$. Both inclusions are strict for the requested distinct reasons.

Use $\mathrm{\Gamma }=(p:C)$, $\mathrm{\Delta }=\cdot$, and the typed simultaneous substitution $\sigma :\mathrm{\Gamma }\to \mathrm{\Delta }$ with $\sigma (p)=u$. Choose binders $a,b\notin \mathrm{supp}(u)\cup \{p\}$. Nominal substitution gives $$(\lambda (a:A).\lambda (b:B).p)[u/p]=\lambda (a:A).\lambda (b:B).u.$$ Translation sends the body occurrence of $p$ to index $2$. The de Bruijn substitution maps the sole free position to $\mathsf{db}(u)$. Its first lift fixes the new zero and weakens the old component; the second repeats that operation. Both paths therefore end at $${\lambda }_A{\lambda }_B({\mathsf{rename}}_{(+1)}({\mathsf{rename}}_{(+1)}\mathsf{db}(u))).$$ If $a$ is replaced by another admissible $a^{\prime }$, nominal equivariance gives $$(a{a}^{\prime })\cdot (t[u/p])=((a{a}^{\prime })\cdot t)[((a{a}^{\prime })\cdot u)/(a{a}^{\prime })(p)].$$ The transposition fixes $p$ and $u$ by the fresh choice. Simultaneously permuting the ordered context and term preserves every lookup position, so both representatives translate to the same de Bruijn term.