Single Substitution

A single substitution in a Context $\Gamma$ is some choice of variable $x:A\in\Gamma$ and a term $\Gamma\vdash e:A$. The action of a single substitution on a term $\Gamma\vdash e^{\prime}:A$ is a term $\Gamma\vdash e^{\prime}[e/x]:A$ where all free occurances of the variable $x$ have been replaced by $e$.

This form of substitution is quite clunky to deal with, and Simultaneous Substitutions should be preferred in almost every case.