The main thing I'm trying to figure is whether (101) itself is a theorem in a constructive setting, whether it is a meta-theorem, or something else.
Andrej Bauer's lecture The Five Stages of Accepting Constructive Mathematics gives the following example of a counterintuitive result in a generic constructive setting. I'm guessing based on the content of his lecture that this generic constructive setting is similar to the usual ZFC but without the axiom of choice, and without the law of the excluded middle. This is only my guess though, I don't know the exact framework that Bauer is assuming for the purposes of this example.
One example that he gave near the start of the lecture is the following (101). Discussion of this example begins at the offset 7:17.
$$ \left\{ x : x \in \mathbb{R} \;\land\; \left( x < 0 \lor x \ge 0 \right) \right\} \subsetneq \mathbb{R} \tag{101} $$
Bauer also claims that the related statement (102) is true.
$$ \mathbb{R} \setminus \left\{x : x \in \mathbb{R} \;\land\; \left(x < 0 \lor x \ge 0\right)\right\} \tag{102} = \{\} $$
(201) and (202) are my two guesses as to what (101) might mean.
(201): (101) is a theorem
I think this just means we can construct a term that witnesses (251).
$$ \left(\left\{ x : x \in \mathbb{R} \land \left(x \ge 0 \lor x < 0\right) \right\} = \mathbb{R}\right) \to \bot \tag{251} $$
(202): (102) is a metatheorem
I interpret this as meaning that, in any model of constructive mathematics, it is not the case that (252).
$$ \left[\left\{ x : x \in \mathbb{R} \land \left(x \ge 0 \lor x < 0\right) \right\}\right] = \left[ \mathbb{R} \right] \tag{252} $$
Where $\left[\psi\right]$ refers to the element of the domain in the model that corresponds to a well-formed formula $\psi$ and $=$ refers to the inherent equality that the model itself is equipped with. Equivalently, $\left[\cdot\right]$ sends closed terms to their interpretation, which I'm pretty sure is a legitimate thing to do.
Best Answer
Disclaimer: There are many foundational theories of constructive mathematics: to answer questions like the one you ask, one has to be explicit about which particular foundation is used. What I say below holds if we choose constructive set theory CZF as our foundational theory. CZF is the theory implicitly used in Bauer's talk, and is the common setting for Bishop's constructive mathematics. Just like in classical mathematics, other foundations are possible, and what I say here does not hold in some of those alternate foundations.
Constructive mathematics is what you get if you remove the law of excluded middle and other principles that imply it from classical mathematics. If you add back the law of excluded middle, you get classical mathematics again (indeed, CZF Set Theory extended with the law of excluded middle is the same as ordinary classical Zermelo-Fraenkel set theory).
This means that you won't be able to prove theorems that contradict established theorems of classical mathematics: if you could prove such a theorem, adding the law of excluded middle would yield an inconsistent theory!
Consequently, (101) is not a theorem of constructive mathematics. For if $S$ denote the set $\{ x \in \mathbb{R} \:|\: x < 0 \vee x \geq 0 \}$, then your (101) can be rephrased as $S \subseteq \mathbb{R} \wedge S \neq \mathbb{R}$. If we could prove $S \neq \mathbb{R}$ in constructive mathematics, then the same proof would work in classical mathematics. But in classical mathematics we can prove $S = \mathbb{R}$, so in that case we could prove both $S \neq \mathbb{R}$ and $S = \mathbb{R}$ in classical mathematics, which would lead to a contradiction.