Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language.

The question is motivated by trying to get a better understanding of the predicative variant of second-order logic studied e.g. by F. Ferreira), which restricts substitution in the $\exists R$ and $\forall L$ rules to quantifier-free formula.

Question: Assume that $\Gamma$ and $\Psi$ are quantifier-free. Assume further that $\Gamma \vdash \exists X. \Psi(X)$ is derivable in intuitionistic propositional SOL. Can we find a quantifier-free formula $T$ such that $\Gamma \vdash \Psi(T)$ is derivable?