[proofplan]
We record the Pi beta computation rule in a presentation of dependent [type theory](/page/Type%20Theory) where this rule is one of the defining judgmental equality rules for Pi types. First, the Pi introduction rule turns the derivation of $b(x):B(x)$ in the extended context into the dependent function $\lambda x.\,b(x)$. Then the dependent substitution rule ensures that substituting $a:A$ for $x$ gives a well-typed term $b[a/x]:B[a/x]$. Finally, the defining beta computation rule for lambda abstraction and application identifies the application $(\lambda x.\,b(x))(a)$ judgmentally with that substituted body.
[/proofplan]
[step:Introduce the dependent function from the term in the extended context]
Let $\Gamma$ be a well-formed context, let $A$ be a type over $\Gamma$, let $B$ be a type family in the extended context $\Gamma,x:A$, and let $b$ denote the term-forming expression satisfying
\begin{align*}
\Gamma,x:A \vdash b(x):B(x).
\end{align*}
By the Pi introduction rule, the lambda abstraction is a term
\begin{align*}
\Gamma \vdash \lambda x.\,b(x):\prod_{x:A}B(x).
\end{align*}
The variable $x$ is bound in $\lambda x.\,b(x)$, so replacing $x$ by an alpha-equivalent fresh variable does not change the term represented by the abstraction.
[/step]
[step:Substitute the argument into the body and its type]
Fix a term $\Gamma \vdash a:A$. Define $B[a/x]$ to be the type obtained by capture-avoiding substitution of $a$ for $x$ in $B(x)$, and define $b[a/x]$ to be the term obtained by capture-avoiding substitution of $a$ for $x$ in $b(x)$. Since $\Gamma,x:A \vdash b(x):B(x)$ and $\Gamma \vdash a:A$, the [citetheorem:9624] gives
\begin{align*}
\Gamma \vdash b[a/x]:B[a/x].
\end{align*}
[guided]
We now check that the expression on the right side of the desired computation rule is well typed. The symbol $b(a)$ in this theorem is not ordinary application of a previously defined function symbol $b$; it abbreviates capture-avoiding substitution into the open term $b(x)$. Thus we define $b[a/x]$ to be the term obtained from $b(x)$ by replacing the free occurrences of $x$ by $a$, avoiding variable capture by alpha-renaming bound variables when necessary. Similarly, $B[a/x]$ is the type obtained from $B(x)$ by the same substitution.
The hypothesis gives a derivable judgment in the extended context:
\begin{align*}
\Gamma,x:A \vdash b(x):B(x).
\end{align*}
The fixed argument gives the derivable judgment:
\begin{align*}
\Gamma \vdash a:A.
\end{align*}
These are exactly the hypotheses of the [citetheorem:9624], applied to the concrete typing judgment $b(x):B(x)$ in the extended context. Therefore substitution preserves derivability and yields
\begin{align*}
\Gamma \vdash b[a/x]:B[a/x].
\end{align*}
This is the typing fact needed for the beta computation rule: after the lambda abstraction is applied to $a$, the resulting body lives in the fiber of the dependent family over $a$.
[/guided]
[/step]
[step:Apply the beta computation rule for lambda abstraction and application]
By Pi elimination, the function application is a well-typed term
\begin{align*}
\Gamma \vdash (\lambda x.\,b(x))(a):B[a/x].
\end{align*}
The defining beta computation rule for Pi types states that applying a lambda abstraction to an argument judgmentally reduces to the capture-avoiding substitution of that argument into the body. Applying this rule to the abstraction $\lambda x.\,b(x)$ and the argument $a$ gives
\begin{align*}
\Gamma \vdash (\lambda x.\,b(x))(a)\equiv b[a/x]:B[a/x].
\end{align*}
Writing $b(a)$ for $b[a/x]$ and $B(a)$ for $B[a/x]$, this is precisely
\begin{align*}
\Gamma \vdash (\lambda x.\,b(x))(a)\equiv b(a):B(a).
\end{align*}
This proves the stated Pi type beta computation rule.
[/step]
