Consider
$$ (\lambda V_1..V_n. E)E_1..E_n $$
Is there a case where application of this form is valid if not all $V_i$ are distinct and some $V_i$ occur free in $E_i$?
Here's an example where it is not valid.
$$ (\lambda xx. \underline{sum} \ xx)(\lambda z.x)(\underline{3}) = (\lambda x. \underline{sum} \ (\lambda z.x) \ x) \ \underline{3} $$
Free variable $x$ in $(\lambda z.x)$ becomes bound in $\underline{sum}$ so this is invalid.
Now I can't find a case where it is valid? Can you give me an example where it is?
Thanks a bunch!
@Spukgespenst from #math libera mentioned
$$ (\lambda xx.x)xx $$
is valid. Thanks!