 Internal form of Löb's theorem

In the Löb's theorem proof, $T⊢\square D\to \square A$ is obtained before any reflection assumption. Put $H=(\square A\to A)$. Propositional reasoning and the diagonal equation give $T⊢H\to D$. Necessitation and distribution yield $T⊢\square H\to \square D$, hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in Gödel-Löb logic, and avoids necessitating a temporary assumption.