Suppose we have the following typed lambda term (where $s$ does not occur in E (which is of type $s \to p$) and $s$ and $s'$ have the same type), and want to apply $\beta$-reduction:
$(\lambda s. E)\, s'$
Every occurrence of $s$ in E must be replaced with $s'$. But suppose there are no occurrences of $s$ in $E$. In this case, does beta reduction lead to (1) or to (2)?
(2) $E\, s'$
I can't see how this is fixed by the definition of beta-reduction.
I have completely rewritten the question to make it clearer.