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
This principle is nonconstructive. Separately, it is incompatible with homotopy type theory.
It is easily checked that an equivalent principle is $\neg \neg \Pi x : A, B_x + \neg B_x$. To show one direction of this, note we clearly have $\Pi x : A, \neg \neg (B_x + \neg B_x)$, and apply your scheme.
This principle is highly nonconstructive. There are many principles compatible with constructive logic that imply $\neg \forall x (P(x) \lor \neg P(x))$ (for some specific domain of quantification and predicate $P$). For example, Brouwer’s continuity principle implies $\neg \forall r \in \mathbb{R} (r = 0 \lor r \neq 0)$.
Separately, even ignoring constructive concerns, your scheme is incompatible with homotopy type theory.
Everything in this paragraph is provable in pure Martin-Löf intensional type theory. Recall the following fact: $(\prod x: A, \prod y: A, x = y \lor x \neq y) \implies \prod x : A, \prod p : x =_A x, p =_{x =_A x} refl_x$. Now note that $(\prod x: A, \prod y: A, x = y \lor x \neq y)$ is clearly logically equivalent to $\prod q : A \times A, p_1(q) = p_2(q) \lor \neg p_1(q) = p_2(q)$. Thus, we must have $\neg \neg \prod x : A, \prod p : x =_A x, p =_{x =_A x} refl_x$.
In terms of homotopy type theory, we just proved that $A$ is not not a set. However, homotopy type theory postulates many types which are not sets. For example, the circle is a type $C$, together with a base point $b : C$, such that the type $b =_C b$ is equivalent to the group of integers.