+\begin{lemma}\label{l:aux2}\r
+ For every \knnf s $\tm$,\r
+ every fresh variable $\var$,\r
+ every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
+ $\nf{(\tm\Subst\var\perm)} \EtaNeq \alpha_j$.\r
+\end{lemma}\r
+\begin{proof}\r
+ By induction on $|\tm|$.\r
+ Let $\tm = \lambda\vec\vartwo.\,h\,\vec a$ and $\sigma\defeq\Subst\var\perm$:\r
+ \begin{itemize}\r
+ \item If $h \neq \var$, then $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h\,\vec {(\nf {a\sigma})}$,\r
+ and we conclude since $h\neq \alpha_j$ by the hypothesis that $\alpha_j$ is\r
+ a fresh variable.\r
+ \item If $h=\var$ and $|\vec a| \leq i$, then\r
+ $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $,\r
+ and we conclude since the head $\varthree'$ is a bound variable,\r
+ while $\alpha_j$ is free.\r
+ \item If $h=\var$ and $|\vec a| > i$, then\r
+ $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
+ $\nf{(\args_i\sigma\,\vec\alpha)} = \tmtwo\,\alpha_j$ by \reflemma{aux1}\r
+ for some inert $\tmtwo$. Clearly $\tmtwo\,\alpha_j \EtaNeq \alpha_j$.\r
+ \end{itemize}\r
+\end{proof}\r