Consider the following theorem about [Heyting arithmetic (HA)](https://en.wikipedia.org/wiki/Heyting_arithmetic)

> For every arithmetical formula $\phi$ whose only free variable is $n$, if $\text{HA} \vdash \forall n. \phi \lor \lnot \phi$ and $\text{HA} \vdash \lnot \lnot \exists n. \phi$, then $\text{HA} \vdash \exists n. \phi$

Or in other words, [Markov's rule](https://en.wikipedia.org/wiki/Markov%27s_principle#Markov's_rule) is [admissible](https://en.wikipedia.org/wiki/Admissible_rule) in Heyting arithmetic.

Proof: $\lnot \lnot \exists n. \phi$ because Heyting arithmetic is sound. By the law of excluded middle, this implies $\exists n. \phi$. Let $k$ satisfy $\phi$. Then by universal instantiation $\text{HA} \vdash \phi[n := \bar k] \lor \lnot \phi[n := \bar k]$ (where $\bar k$ is $1 + 1 + \dots + 1 + 0$ with $1 +$ repeated $k$ times). By the disjunction rule, either $\text{HA} \vdash \phi[n := \bar k]$ or $\text{HA} \vdash \lnot \phi[n := \bar k]$. The second case is impossible since Heyting arithmetic is sound. Thus $\text{HA} \vdash \phi[n := \bar k]$ which implies $\text{HA} \vdash \exists n. \phi$.  
$\square$

Call this theorem T. **What is the reverse mathematical strength of T?** For example, is it equivalent to one of the [big five](https://en.wikipedia.org/wiki/Reverse_mathematics#The_big_five_subsystems_of_second-order_arithmetic)?

First observation: T is weaker than Con(PA) over Peano arithmetic. Proof: Assume that Peano arithmetic proves that T implies Peano arithmetic is consistent. However, not-T also proves Peano Arithmetic is consistent because it implies there is a statement of the form $\exists n. \phi$ that Peano arithmetic can't prove. Thus Peano arithmetic proves Con(PA), which would violate Gödel's second incompletes theorem. $\square$

However, $T$ doesn't seem entirely trivial. Since Heyting arithmetic doesn't have Markov's property, constructing the proof for $\text{HA} \vdash \exists n. \phi$ seems to require a bit of proof theory and induction.

(Note that since $T$ is $\Pi_2^0$, it shouldn't make much of a difference whether the meta-theory is classical or constructive.)