[proofplan]
The proof is exactly the dependent eliminator for the W-type $W_{a:A}B(a)$, specialized to the motive $P:W\to\mathcal U$. The only data required by this eliminator is a branch for the unique constructor $\operatorname{sup}$: given $a:A$, a subtree function $f:B(a)\to W$, and induction hypotheses for all immediate subtrees $f(b)$, one must produce an element of $P(\operatorname{sup}(a,f))$. The assumed function $h$ is precisely that branch, so applying the W-type eliminator to $P$ and $h$ gives the required dependent function on all of $W$.
[/proofplan]
[step:Package the induction step as the constructor branch]
By hypothesis, we are given a dependent function
\begin{align*}
h:\prod_{a:A}\prod_{f:B(a)\to W}\left(\prod_{b:B(a)}P(f(b))\right)\to P(\operatorname{sup}(a,f)).
\end{align*}
For each $a:A$ and each function
\begin{align*}
f:B(a)\to W,
\end{align*}
define the corresponding constructor branch
\begin{align*}
H(a,f):\left(\prod_{b:B(a)}P(f(b))\right)\to P(\operatorname{sup}(a,f))
\end{align*}
by
\begin{align*}
H(a,f):=h(a)(f).
\end{align*}
Thus, if
\begin{align*}
\operatorname{ih}:\prod_{b:B(a)}P(f(b))
\end{align*}
is a family of induction hypotheses indexed by the immediate subtrees $b:B(a)$, then
\begin{align*}
H(a,f)(\operatorname{ih})=h(a)(f)(\operatorname{ih}):P(\operatorname{sup}(a,f)).
\end{align*}
[/step]
[step:Apply the dependent eliminator for the W-type]
We now use the dependent eliminator supplied by the W-type rules. This eliminator states that, for every motive
\begin{align*}
P:W\to\mathcal U,
\end{align*}
a constructor branch of type
\begin{align*}
\prod_{a:A}\prod_{f:B(a)\to W}\left(\prod_{b:B(a)}P(f(b))\right)\to P(\operatorname{sup}(a,f))
\end{align*}
determines a dependent function
\begin{align*}
\prod_{w:W}P(w).
\end{align*}
The branch required by this eliminator is exactly $H$, which was defined from $h$ in the preceding step. Therefore the eliminator gives a term
\begin{align*}
\operatorname{ind}_{W,P}(h):\prod_{w:W}P(w).
\end{align*}
[guided]
The W-type $W=W_{a:A}B(a)$ has one constructor, namely
\begin{align*}
\operatorname{sup}:\prod_{a:A}(B(a)\to W)\to W.
\end{align*}
Thus every element introduced into $W$ has the form $\operatorname{sup}(a,f)$, where $a:A$ is a label and
\begin{align*}
f:B(a)\to W
\end{align*}
assigns to each position $b:B(a)$ an immediate subtree $f(b):W$.
To prove a dependent predicate
\begin{align*}
P:W\to\mathcal U
\end{align*}
for all $w:W$, the dependent W-type eliminator asks for one constructor case. In that case, we must assume that $P$ already holds for all immediate subtrees. Formally, for fixed $a:A$ and $f:B(a)\to W$, the induction hypotheses are packaged as a dependent function
\begin{align*}
\operatorname{ih}:\prod_{b:B(a)}P(f(b)).
\end{align*}
The target for the constructor case is then
\begin{align*}
P(\operatorname{sup}(a,f)).
\end{align*}
The hypothesis of the theorem supplies exactly this operation. It gives
\begin{align*}
h:\prod_{a:A}\prod_{f:B(a)\to W}\left(\prod_{b:B(a)}P(f(b))\right)\to P(\operatorname{sup}(a,f)).
\end{align*}
Therefore, for each $a:A$, each $f:B(a)\to W$, and each family of induction hypotheses
\begin{align*}
\operatorname{ih}:\prod_{b:B(a)}P(f(b)),
\end{align*}
we may form
\begin{align*}
h(a)(f)(\operatorname{ih}):P(\operatorname{sup}(a,f)).
\end{align*}
This is precisely the constructor branch required by the dependent eliminator for $W$.
Applying that eliminator with motive $P$ and branch
\begin{align*}
(a,f,\operatorname{ih})\mapsto h(a)(f)(\operatorname{ih})
\end{align*}
produces a dependent function
\begin{align*}
\operatorname{ind}_{W,P}(h):\prod_{w:W}P(w).
\end{align*}
The recursive calls are permitted exactly on the immediate subtrees $f(b)$, and the W-type eliminator is the rule asserting that this well-founded recursive definition determines a term on all of $W$.
[/guided]
[/step]
[step:Identify the eliminator output with the required induction function]
The term obtained from the dependent eliminator has type
\begin{align*}
\prod_{w:W}P(w).
\end{align*}
This is exactly the conclusion of the theorem. Hence, from the assumed step function $h$, we have constructed the dependent induction function
\begin{align*}
\operatorname{ind}_{W,P}(h):\prod_{w:W}P(w).
\end{align*}
[/step]
