Prawitz's conjecture on completeness of intuitionistic logic for the theory of grounds

An operational type is a specification of the premises and conclusion of a rule together with the domains and co-domains governing its discharged assumptions. Let $\tau_1,\ldots,\tau_n\rhd\tau_{n+1}$ be an operational type, and suppose that $f$ is a universal operation on grounds of this type. For each $i\leq n$, let $\sigma_i$ be $\tau_i$ when $\tau_i$ has empty domain, and otherwise let $\sigma_i$ be a derivation from $\Gamma_i$ to $\alpha_i$, where $\Gamma_i$ and $\alpha_i$ are respectively the domain and co-domain of $\tau_i$. Let $R$ be the inference with premises $\sigma_1,\ldots,\sigma_n$ and conclusion $\beta$, and let $\beta$ be the co-domain of $\tau_{n+1}$. The bindings of $f$ and $R$ agree: $f$ binds $x$ and $\xi^\gamma$ at index $i$ exactly when $R$ binds $x$ and discharges $\gamma$ on $\sigma_i$. Prawitz's conjecture. If there is a universal operation on grounds $f$ of operational type $\tau_1,\ldots,\tau_n\rhd\tau_{n+1}$, then the corresponding inference $R$ is derivable in intuitionistic logic, $\texttt{IL}$. This conjecture is the completeness question for $\texttt{IL}$ with respect to the theory of grounds: correctness is established, while the conjecture would imply the converse implication $\Gamma\models\alpha\Rightarrow\Gamma\vdash_{\texttt{IL}}\alpha$.