I understand how to proof the deduction theorem $$(D): \Delta,\varphi\vdash\psi\Rightarrow\Delta\vdash\varphi\rightarrow\psi$$ with a set of propositions $\Delta$ and some propositions $\varphi$ and $\psi$ for propositional logic. If I understand correctly, it works via induction over the length of a proof n. Then we show that for n=1, $\psi$ must be either equal to $\varphi$, in which case the implication $\varphi\rightarrow\psi$ is trivially provable, or it is a member of $\Delta$ in which case we have $\Delta\vdash\psi$ and with the tautology $\psi\rightarrow(\varphi\rightarrow\psi)$ and MP we have $\varphi\rightarrow\psi$. Then we assume that for a proof of length n the above statement (D) holds true and conclude, that it must hold true for a proof of length n+1. We proceed as follows: $\psi$ must be reached via MP, so there is a proposition $\phi$, s.t. $\phi\rightarrow\psi$ and $\phi$ are proved from $\Delta,\varphi$ in a maximum of n steps. By our induction hypothesis we have $\Delta\vdash\varphi\rightarrow\phi$ and $\Delta\vdash\varphi\rightarrow(\phi\rightarrow\psi)$, so by the tautology $(\varphi\rightarrow(\phi\rightarrow\psi)\rightarrow((\varphi\rightarrow\phi)\rightarrow(\varphi\rightarrow\psi))$ using MP twice we have $\Delta\vdash\varphi\rightarrow\psi$ as desired.
Now as far as I understood proving (D) for predicate logic when using tautologies and tautological consequences everything is the same (assuming that $\psi$ is a sentence), we only have to consider one further step how to reach $\psi$ and that is generalization (I assume because specification can be somehow reduced?). But how does the reasoning work here exactly? I assume that (D) holds true for a proof of length n and have to show that it holds for a proof of length n+1. So let's assume we reach $\psi$ via generalization, that means that $\psi=\forall{x}\psi'$ and in our proof of length n we have the line $\psi'$ - how do I use the induction hypothesis here?
The deduction theorem for predicate logic follows the same line of ideas as the deduction theorem for propositional calculus except for one restriction: The generalised variable in the consequent formula must not occur free in the antecedent formula.
For the systems that employ the axiom $$\forall x(A\rightarrow B)\rightarrow(\forall x A\rightarrow\forall x B)$$
the referred variable is already bound. For the systems that employ the axiom
$$\forall x(A\rightarrow B)\rightarrow(A\rightarrow\forall x B)$$
the restriction must be observed.
I shall go over the baseline of the relevant part of the proof without full annotation, since the steps are sufficiently clear.
Suppose $\psi$ is deduced by either
The former prong of the fork is as in the familiar one of propositional calculus. We look into the latter prong. Hence, we have got $\psi_{j}$ for some $j$ in the sequence. Then,
$\phi\rightarrow\psi_{j}$ by induction hypothesis.
$\forall x_{i}(\phi\rightarrow\psi_{j})$ by generalisation where the variable $x_{i}$ does not occur free in $\phi$.
$\forall x_{i}(\phi\rightarrow\psi_{j})\rightarrow(\phi\rightarrow\forall x_{i}\psi_{j})$ by the axiom mentioned above.
$\phi\rightarrow\forall x_{i}\psi_{j}$ by modus ponens.
Therefore,
$$\Delta,\phi\vdash\psi\implies\Delta\vdash\phi\rightarrow\psi$$