In fact I'm interested in a (preferably constructive) proof of the meta-implication: $T\vdash[\exists x B(x)\to B(c)]\to A $ implies $T\vdash A $ , where $c$ is a new constant for $T, B$ and $A$ and the proof system in hand is intuitionistic Natural Deduction.
Just to note, I cannot use $(B\to A)\leftrightarrow (\neg B\vee A)$ nor the prenex operations as in standard proofs for classical theories.
A "classical" proof is based on the Theorem on Constants: Let $T'$ be obtained from $T$ by adding new constants (but no new nonlogical axioms); then, for every formula $A$ of T and every new constant $c$, $T \vdash A(x)$ iff $T' \vdash A[c/x]$.
With it, it follows that if $T \vdash (\exists x B(x) \to B[c/x]) \to A$, then $T \vdash (\exists x B(x) \to B[y/x]) \to A$, where $y$ is a new variable.
Hence, by $\exists$-introduction:
Now :$T \vdash \exists x B \to \exists y B[y/x]$, and thus: $T \vdash \exists y \ (\exists x B \to B[y/x])$ by the prenex operations.
Finally, by modus ponens:
Unfortuantely, the "prenex operation" step is not allowed in intuitionistic logic.