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](https://link.springer.com/article/10.1007/s10992-005-9001-z)), 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?