Simultaneous Substitution

A simultaneous substitution $\Gamma\to\Delta$ is a term $\Gamma\vdash x:A$ for each $A\in\Delta$. In other words, it is a Telescope of terms.

Simultaneous substitutions have some technical benefits over Single Substitutions; in particular, they make performing substitution under binders much easier, as we can simply extend the substitution with a variable.