I am looking for a proof of and/or a reference for the result that Markov's principle can be proved in the framework of constant domain logic. By constant domain logic, I mean intuitionistic logic plus the axiom


$\forall x(P(x) \,\vee\, Q) \to \forall xP(x) \,\vee\,Q \quad$ where x is not free in $Q$.


This result is alluded to, without proof, in the entry about intuitionistic logic in the Stanford encyclopedia of philosophy:
<https://stanford.library.sydney.edu.au/archives/fall2008/entries/logic-intuitionistic/#KriSemForIntLog> (I have found no other reference.)



Markov's principle from constant domain logic
Emil Jeřábek answered in a comment:


$\forall x(A(x) \vee \neg A(x)) \:\to\: \forall x (\exists y A(y) \vee \neg A(x))
\:\to\: \exists y A(y) \vee \forall x(\neg A(x))$


So, that’s even stronger than MP: decidability is preserved by existential quantification.


