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.)