Intuitionistic proof of $\forall x(P(x)\lor Q(x))\to(\forall x P(x)\lor\exists x Q(x))$ Similar to Is $ \forall x(P(x) \lor Q(x)) \vdash \forall x P(x) \lor \exists xQ(x) $ provable?, but with intuitionistic logic. I expect it is not, since I don't think the $\exists x Q(x)$ on the right is very "constructive", but curiously the finite version of this
$$((p_1\lor q_1)\land(p_2\lor q_2))\to((p_1\land p_2)\lor(q_1\lor q_2))$$
is intutitionistically provable, since you can break up the left side into four cases and verify that each satisfies the right side.
 A: No, it is not intuitionistically valid. Here is a Kripke model where it doesn't hold:
There are two frames, $w$ and $u$ with $w<u$.
In $w$ the universe is $\{\mathtt a\}$ and $P(\mathtt a)$ is true.
In $u$ the universe is $\{\mathtt a,\mathtt b\}$, and $P(\mathtt a)$ and $Q(\mathtt b)$ are true.
Then both frames satisfy $\forall x(P(x)\lor Q(x))$.
However $w$ doesn't satisfy $\forall x\,P(x) \lor \exists x\,Q(x)$. The first disjunct is false because the intuitionistic interpretation of $\forall$ must be true in all reachable frames (and it clearly isn't true in $u$), and the second is clearly false in $w$.
A: Just for the record, here's an answer using the open set model. What we have to do is find families of open sets $P_i$ and $Q_i$ in some topological space $X$ such that:
$$
Int(\bigcap_i(P_i \cup Q_i)) \not\subseteq Int(\bigcap_i P_i) \cup (\bigcup_i Q_i) \tag*{(*)}
$$
To do this, take $X$ to be the unit interval $[0, 1]$ and for $i = 1, 2, \ldots$ define
$$
P_i = [0, \frac{1}{i}) \\
Q_i = (\frac{1}{i+1}, 1]
$$
Since $X = P_i \cup Q_i$ for any $i$, the left-hand side of $\mbox{(*)}$ is equal to $X$. However, $\bigcap_i P_i = \{0\}$, which has empty interior, so the right-hand side of (*) is $\bigcup_i Q_i = (0, 1] \not \supseteq X$.
