Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

BISH famously includes the full axiom of choice scheme (in the functional language of second-order arithmetic), which is utterly weak in that context but very strong when combined with the law of the excluded middle. This is precisely the context in which Bishop wrote that the axiom of choice follows from "the very meaning of existence".

Thus there are formulas of second-order arithmetic provable in BISH that are not even provable in $Z_2$, the system of clasical second-order arithmetic with full induction and comprehension.

Maybe it is interesting that for $CT$ (Church thesis) $BISH+CT$ is consistent, but $RCA_0\vdash \neg CT$. By $CT$ I mean axiom scheme of $CT$ for every formula.

$CT-scheme$: For every first order formula $\psi(x,y)$, $\forall x \exists y \psi(x,y)\rightarrow \exists e\forall x\exists y(\psi(x,y)\land \phi(e,x,y)$ where $\phi(e,x,y)$ is kleene predicate.

Also let $U(e,x,y)$ be a first order formula such get godel number of a formula like $\eta(x,y)$ in $e=\ulcorner \eta(x,y) \urcorner$, gets $x,y$ and simulates $\eta(x,y)$, then $CT$ can be formalized in one axiom like this: $$CT:=\forall u\exists e(\forall x\exists y U(u,x,y)\rightarrow \forall x\exists y(U(u,x,y)\land \phi(e,x,y)))$$ Define $$h(n)=\left\{\begin{matrix} 1,\exists x\phi(n,n,x)\\ 0, \forall x \neg \phi(n,n,x) \end{matrix}\right.$$ This function can represent by formula $H(n,y):=(\exists x\phi(n,n,x)\land y=1)\lor(\forall x\neg\phi(n,n,x)\land y=0)$, trivially $RCA_0\vdash \forall n \exists y H(n,y)$, therefore $RCA_0\vdash \neg CT$, but $BISH+CT\nvdash \bot$, similar arguments work if we take axiom scheme of $CT$ instead of $CT$

The intermediate value theorem seems to be provable in $RCA_0$ but is certainly not provable in the usual form in $BISH$. I am relying on Wikipedia.