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