This rings a bell. And ah yes, on p. 48 of Sara Negri and Jan van Plato's admirable book Structural Proof Theory (CUP, 2001), they write
It is not the [general] feature of having a multiset as a succedent that leads
to classical logic, but the unrestricted $R\!\supset$ rule,
where by the unrestricted $R\!\supset$ they mean your classical $\to\! R$ rule, and the restricted rule would be your $\to\! R'$ rule.
Then on p. 108, they introduce an intuitionistic multisuccedent calculus they call G3im, which is exactly like a classical multisuccedent calculus except for the $\supset$ rules (though both left and right rules get tinkered with). I guess that the ensuing discussion, and the 1988 book by Dragalin Mathematical Intuitionism to which the calculus is due, would seem to be good starting points for further investigation (and I'd be interested to hear more about how things go!).
We want to find a proof term for the following type:
$$ (\forall x: A. \exists y: A. R(x,y)) \to \forall x: A. \exists f: \mathbb{N} \to A. f(0) = x \,\land\, \forall n: \mathbb{N}. R(f(n), f(\mathsf{succ}(n)))$$
Let $h: \forall x: A. \exists y: A. R(x, y)$, and $x : A$. We need to exhibit a function $f: \mathbb{N} \to A$ and a proof term for the required property. Intuitively, we want $f$ such that
$$\left\{\begin{array}{l} f(0) = x\\ f(\mathsf{succ}(n)) = \pi_1 (h(f(n))) \end{array}\right.$$
therefore we let $f = \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y)))$. Then you have that $f(0)$ normalizes to $x$, and so $\mathsf{id}(x)$ is a proof of $f(0) = x$. Now, let $n: \mathbb{N}$. We want to prove that $R(f(n),f(\mathsf{succ}(n)))$. But this is given precisely by $\pi_2 (h(f(n)))$, since $f(\mathsf{succ}(n))$ normalizes to $\pi_1 (h(f(n)))$. In conclusion, a proof term for the proposition would be:
$$\lambda h: \forall x: A. \exists y: A. R(x, y). \lambda x: A.\\ \langle \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y))),\\ \langle \mathsf{id}(x), \lambda n: \mathbb{N}. \pi_2 (h(\mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y))))) \rangle \rangle $$
Best Answer
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$.