Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?, when does $$\forall x \in [a,b] \cup [b,c]. f(x) = g(x)$$ imply that $f = g$?
If $S = \mathbb R$, it is true.
Proof: Let $x \in [a,c]$. Assume that $f(x)$ does not equal $g(x)$. Assume $x < b$. Thus $x \in [a,b]$, implying $f(x) = g(x)$, a contradiction. Thus $b \le x$, implying $x \in [b,c]$, implying $f(x) = g(x)$, a contradiction. Thus $f(x)$ does not not equal $g(x)$. Since $\mathbb R$ has stable equality, $f(x)$ equals $g(x)$. $\square$
This of course applies for any $S \subseteq \mathbb R$ as well. In fact, this proof works for any $S$ with stable equality.
On the other hand, there are examples where the property is constructively unprovable.
Proof: Let $o$ be any object, and consider
$$S = \{\{o : y \in [a, b] \cup [b, c]\} : y \in [a,c]\}$$
$$f(x) = \{o : x \in [a,b] \cup [b,c]\}$$
$$g(x) = \{o : b \in [a,b] \cup [b,c]\} = \{o\}$$
Then for all $x \in [a,b] \cup [b,c]$, we have $f(x) = \{o\} = g(x)$. But $f = g$ implies that for any $x \in [a,c]$ we have $o \in \{o : x \in [a,b] \cup [b,c]\}$, implying $x \in [a,b] \cup [b,c]$. Thus $[a,c] = [a,b] \cup [b,c]$, implying the analytic LLPO is provable. But the analytic LLPO is constructively taboo, and thus $f = g$ is unprovable. $\square$
This of course also applies to any superset of $S$, such as $\mathcal P(\{o\})$. (This example was inspired by Gro-Tsen's answer.)
