Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language. Predicative SOL (studied e.g. by [F. Ferreira](https://link.springer.com/article/10.1007/s10992-005-9001-z)) denotes the variant of SOL in the same language which restricts the quantifier rules of SOL

$$\frac{\Gamma \vdash \varphi[X:=A]}{\Gamma \vdash \exists X. \varphi} \ \ \ \ \ \ \ \ \ \ \ \ \frac{\Gamma, \varphi[X:=A] \vdash \Delta}{\Gamma, \forall X.\varphi \vdash \Delta}$$

by requiring that $A$ be a quantifier-free formula.

**Question:** How conservative is full SOL over its predicative variant? In particular, consider a sequent $\Gamma \vdash \exists X. \varphi$ in which $\Gamma$ and $\varphi$ are both quantifier-free. If $\Gamma \vdash \exists X. \varphi$ has a SOL-proof, does it always have a Predicative SOL proof?