such that, for all $K\subseteq Z$, $I\cup J_I\cup K\models \phi$. As can be verified by the properties of $\Phi$-reductions, then there is no model $M\subset M'[I,J_I]$ of $P^{M'[I,J_I]}$. Consequently, there is also no such model of $(P\cup F)^{M'[I,J_I]}$, and thus $M'[I,J_I]\in{{\mathit AS}}(P\cup F)$.

So in each of these cases ${{\mathit AS}}(P\cup F) \neq \emptyset$ and since these cases cover all possible $F \subseteq U$, we obtain that $P$ is super-coherent.

In total we have shown that $\Phi$ being false implies that any $\Phi$-reduction $P$ is not super-coherent, while $\Phi$ being true implies that any $\Phi$-reduction is super-coherent, which proves the lemma.

It remains to show that for any QBF of the desired form, a $\Phi$-reduction can be obtained in polynomial time (w.r.t. the size of $\Phi$). For the construction below, let us denote a negated atom $a$ in the propositional part of the QBF $\Phi$ as $\overline{a}$.

\[def:phi\_program\] For any QBF $\Phi = \forall X\exists Y\forall Z\phi$ with $\phi=\bigvee_{i=1}^n l_{i,1}\land\cdots\land l_{i,m_i}$ a DNF (i.e., a disjunction of conjunctions over literals), we define $$\begin{aligned}
\label{eq:red:first}
P_\Phi & = & 
\{  x \lor \overline{x} {\leftarrow};\;
u {\leftarrow}x,\overline{x};\;
w {\leftarrow}x,\overline{x};\;
x {\leftarrow}u,w;\;
\overline{x} {\leftarrow}u,w\mid x\in X\}\cup{}\\
&&
\{  y \lor \overline{y} {\leftarrow}v;\;
u 