Preservation under Substitution with Telescopes In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":


If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$,
then $\Gamma \vdash [v/x]t : \tau_2 $.


However, the proof of this relies on the property of permutation, that we can rearrange contexts and it will preserve typing of terms.

I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in $\Gamma$ and $\tau_2$ as well.

Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?
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.