Substitution lemma for types
The substitution lemma only holds if what you're substituting is well-formed: $S$ can only contain type variables listed in $E$. In the application of T-TApp, $Y$ is a fresh variable, not present in $E,X,\Delta$. In particular, $Y \ne X$, $Y \notin S$ and $Y \notin A$.

There several ways to model variable names and renaming.


Shadowing allows a binder inside another binder to use the same name (e.g. $\lambda x. \lambda x. M$), and then the outer name is hidden (shadowed) in the inner construct (any occurence of $x$ in $M$ refers to the inner $x$). If you want to refer to the outer variable (which can happen to perform a beta reduction, for example), you need to first perform an explicit alpha conversion to rename one of the variables.
Implicit renaming always uses distinct names for any two binders present anywhere in an expression (so you never write $\color{red}{\lambda x. \lambda x. M}$ or even $\color{red}{(\lambda x. M) (\lambda x. M)}$, but $\lambda y. \lambda x. M$ and $(\lambda x.M) (\lambda y.[x \mapsto y]M)$), and there is an implicit alpha conversion after any reduction that duplicates a term. This is called the Barendregt convention.
Most literature claims to use the Barendregt convention, but in fact uses an intermediate convention where there nested binders never use the same name, but binders that don't overlap each other can use the same name, and there is an implicit alpha conversion step immediately after shadowing occurs. So for example $(\lambda x.M) (\lambda x.M)$ is allowed in writing, but the meta-notation $x$ in the two subterms are supposed to represent two different variables. As far as I remember, TAPL uses this convention.


An environment is a collection of binders, so without shadowing, it cannot define the same variable name more than once (no $\Gamma_1,X,\Gamma_2,X,\Gamma_3$).

Now, let's look at the application of T-TApp. The premise is $\Gamma' \vdash t' : \forall Y. T'$ where $\Gamma' = (E, [X \mapsto S] \Delta)$, $t' = [X \mapsto S] t$ and $T' = [X \mapsto S] T$. From this premise, you can conclude
$$\Gamma' \vdash \lambda t'[A'] : [Y \mapsto A'] T'$$
for any well-formed $A'$. You want to prove $\Gamma' \vdash [X \mapsto S] (t[A]) : [X \mapsto S] [Y \mapsto A] T$. So take $A' = [X \mapsto S] A$. The conclusion is
$$\Gamma' \vdash ([X \mapsto S] t)[[X \mapsto S] A] : [Y \mapsto [X \mapsto S] A] [X \mapsto S] T$$
and this is indeed
$$\Gamma' \vdash [X \mapsto S] (t[A]) : [X \mapsto S] [Y \mapsto A] T$$
since $Y \ne X$ and $Y \notin S$.