the following proposition is presented:
PROPOSITION I. If $\alpha \in Ty2^-$ is $\lambda$-reduced and $\beta$ is a 2-functor occurring in $\alpha$, then either:
(a) $\beta$ contains a free variable alien to $IL^+$, or
(b) $\beta$ is of the form $(\lambda x. \,\gamma)$.
The following definition is given prior to this:
for any $\tau \in IT^+$, $Ty2_{\tau}^-$ is the set of all $\alpha \in Ty2$, satisfying: (a) if $x \in Var_{\tau}$, occurs freely in $\alpha$, then $\tau \in IT^+$, and (b) if $c \in Con_{\tau}$, occurs in $\alpha$, then $\tau = \langle s, \tau' \rangle$ for some $\tau' \in IT$.
This defines $Ty2_{\tau}^-$, for arbitrary $\tau$, so that, presumably $Ty2^-$ is defined as:
$$Ty2^{-} = \{\alpha \in Ty2 \mid \text{for some } \tau \in IT^+: \text{ if } x \in Var_{\tau} \text{ occurs freely in } \alpha \text{ then } \tau \in IT^+ \text{ and if }c \in Con_{\tau} \text{ occurs in } \alpha, \text{ then } \tau = \langle s, \tau' \rangle \text{ for some } \tau' \in IT \}$$
According to clause (a) of PROPOSITION 1, If $\alpha \in Ty2^-$ is $\lambda$-reduced and $\beta$ is a 2-functor occurring in $\alpha$, then one possibility is that $\beta$ contains a free variable alien to $IL^+$. But how can $\beta \in Ty2^{-}$ contain a free variable alien to $IL^+$ when all the formulas in $Ty2^{-}$ contain only free variables which are in $IL^+$, by the definition of $Ty2^{-}$?