 Here is a proof that the rule “If \(\forall x (A \vee B(x))\) is a theorem, so is \(A \vee \forall x B(x)\)” (where \(x\) is not free in \(A)\) is not admissible for \(\mathbf{HA},\) if \(\mathbf{HA}\) is consistent. Gödel numbering provides a quantifier-free formula \(G(x)\) which (numeralwise) expresses the predicate “\(x\) is the code of a proof in \(\mathbf{HA}\) of \((0 = 1).\)” By intuitionistic logic with the decidability of quantifier-free arithmetical formulas, \(\mathbf{HA}\) proves \(\forall x(\exists y G(y) \vee \neg G(x)).\) However, if \(\mathbf{HA}\) proved \(\exists yG(y) \vee \forall x\neg G(x)\) then by the disjunction property, \(\mathbf{HA}\) must prove either \(\exists yG(y)\) or \(\forall x\neg G(x).\) The first case is impossible, by the existence property with the consistency assumption and the fact that \(\mathbf{HA}\) proves all true quantifier-free sentences. But the second case is also impossible, by Gödel’s second incompleteness theorem, since \(\forall x\neg G(x)\) expresses the consistency of \(\mathbf{HA}.\)