Preservation under Substitution with Telescopes
The most general form of substitution theorems speaks about arbitrary contexts:


Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (it's a simultaneous substitution giving a term $\Gamma \vdash e : A$ for every $y : A$ appearing in $\Delta$, and in case of type dependencies we have to do it recursively).
Prove that if $\Delta \vdash e : A$ then $\Gamma \vdash e\sigma : A\sigma$.


In such generality there is no reliance on exchange rules and it all works in dependent type theory as well. The case suggested by Max New in his answer is a special case.