 The hypothesis is needed because not all arithmetical formulas are decidable in \(\mathbf{HA}.\) However, \(\forall x\forall y(x = y \vee \neg(x = y))\) can be proved directly by mathematical induction, and so: 