The substitution lemma connects variable replacement with typing. In the simply typed lambda calculus it states:

if

$$\Gamma,x:S\vdash e:T$$

and

$$\Gamma\vdash v:S,$$

then

$$\Gamma\vdash e[v/x]:T.$$

In words: if expression $e$ is well typed when it may use $x$ as a value of type $S$, then replacing the free occurrences of $x$ by any well-typed value of type $S$ preserves the type of $e$.

For example, suppose

$$x:\text{Int}\vdash x+1:\text{Int}$$

and

$$\vdash 4:\text{Int}.$$

Then the lemma gives

$$\vdash (x+1)[4/x]:\text{Int},$$

that is,

$$\vdash 4+1:\text{Int}.$$

The proof proceeds by structural induction on the typing derivation for $e$. The function-abstraction case requires care with bound names: alpha-renaming avoids variable capture before substitution descends under a binder.

This lemma is crucial because beta reduction performs substitution. It supplies the formal bridge needed to prove that evaluating a well-typed function application cannot destroy its type.