+ Let $\sigma \defeq \Subst\var\perm$.\r
+ First of all, note that by \reflemma{k-prime-nf}\r
+ $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and\r
+ are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$.\r
+ \r
+ If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$.\r
+ Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that\r
+ $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.\r
+ Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and \r
+ $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,\r
+ with $|\vec\vartwo| = \xK$.\r
+ By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,\r
+ and by cases on the definition of eta-difference:\r
+ \begin{itemize}\r
+ \item $h_1 \neq h_2$: we distinguish three subcases.\r
+ \begin{itemize}\r
+ \item $h_1,h_2\neq \var$:\r
+ it follows that $\nf{\tm\sigma} = \nf{(\lambda\vec\vartwo.\,h_1\,\vec a)\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
+ and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
+ and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because\r
+ their head variables are different.\r
+ \item $h_1=\var$ and $h_2\neq \var$: \TODO\r
+ \item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.\r
+ \end{itemize}\r
+ \item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:\r
+ if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
+ and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
+ and we conclude because the two terms have a different number of arguments.\r
+ \r
+ We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
+ \begin{itemize}\r
+ \item Both $|\vec a|,|\vec b|\leq i$: \TODO\r
+ \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
+ \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
+ plus another one. Reason on the numebr of arguments\r
+ $\Args{\nf{a_i\sigma\vec\alpha}}$ vs \r
+ $\Args{\nf{b_i\sigma\vec\alpha}}$.\r
+ If equal conclude, otherwise conclude by lemma above.\r
+ \end{itemize}\r
+ \item \r
+ $h_1 = h_2$ and $|\vec a| = |\vec b|$\r
+ but $a_n \EtaNeq b_n$ for some $n$.\r
+ If $h_1=h_2\neq\var$, then again\r
+ $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =%\r
+ \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
+ and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that \r
+ $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.\r
+ {\color{red}[Can we use the \ih{} here?]}\r
+ \r
+ We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
+ \begin{itemize}\r
+ \item $|\vec a| = |\vec b| \leq i$: \TODO easy \r
+ \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok\r
+ \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO\r
+ by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$\r
+ and conclude by appending the $\vec a$ and $\vec b$.\r
+ \end{itemize}\r
+ \end{itemize}\r