 Full local reflection in a one-sentence extension is inconsistent

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If $T+X$ proves ${\mathrm{Pr}}_T(┌Y┐)\to Y$ for every sentence $Y$, then $T⊢\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T⊢X\to (\square \neg X\to \neg X)$. This propositionally implies $T⊢\square \neg X\to \neg X$, and Löb's theorem gives $T⊢\neg X$. A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.