Head variables of terms after application We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\lambda y_1 y_2 \ldots y_n . y_i u_1 u_2 \ldots u_m$. In this case, we shall say that $i$ is the index of this term.

My question is, does every term of a type with multiple components (that is, $n$ is greater than $1$ in the example above) behave as a function with respect to indices? Namely, given two terms of the same index of type $A_1$ above, would both return terms of type $A_2\ldots\rightarrow A_n \rightarrow 0$ with the same index?
Here's a counterexample to your conjecture.

$$
\begin{array}{lcl}
M &amp; : &amp; ((0 \to 0 \to 0) \to 0 \to 0 \to 0) \to 0 \to 0 \to 0 \\
M &amp; = &amp; \lambda\,f\,x\,y.\;f\;(\lambda\,a\,b.\;f\;(\lambda\,u\,v.\;u)\;a\;b)\;x\;y
\end{array}$$

This beta-normal, eta-long with index 1. Now, consider the two following terms, both also of index 1:

$$
\begin{array}{lcl}
N &amp; = &amp; \lambda\,p\,x\,y.\;p\;x\;y \\ 
N' &amp; = &amp; \lambda\,p\,x\,y.\;p\;y\;x \\ 
\end{array}
$$

Now, $M\;N$ reduces to $\lambda\,x\,y.\;x$ (index 1) and $M\;N'$ reduces to $\lambda\,x\,y.\;y$ (index 2).