This question is about the 'unique extension property' as defined here, which is: A topological space $Y$ has the unique extension property if, for any topological space $X$, any two continuos functions from $X$ into $Y$ which agree on a dense subset of $X$ are equal. This property is equivalent to the set $Y$ being Hausdorff as has been proved in the mentioned article as well as in a previous question here.
My question is, can it be proved that the unique extension property implies Hausdorffness without using LEM, that is, without using the contrapositive? (Preferably without using the axiom of choice)
The proof that UEP implies Hausdorff can also be given thusly: let $x \neq y$ in $X$.
Then consider $X \times X$ in the product topology and let $f_1$,$f_2$ be the two continuous projections and let $D:=\{(x,x) \mid x \in X\}$. Then $D$ is by definition dense in $Y=\overline{D}$ (closure taken in $X \times X$) and $f_1 \restriction_D = f_2\restriction_D$ and so $f_1 = f_2$ on $Y$ which means that $\overline{D} = D$ as $f_1 \neq f_2$ outside $D$, in particular $x=f_1(x,y)=f_2(x,y)=y$.
So $(x,y) \notin \overline{D}$ which means that there is a (basic) open neighbourhood $U \times V$ of $(x,y)$ that misses $D$, and this implies $U \cap V = \emptyset$.
But to avoid the LEM you'd have to set up topology in quite a different way. See intuitionistic topology and such theories. Some use of proofs by contradiction, or use of the contrapositive is unavoidable, and shouldn't be avoided unless one is a very strict constructivist/intuitionist/finitist etc., in which case you have to throw away most of standard maths anyway. I think the above argument could be acceptable to the OP, I hope. It's inspired on the fact that $X$ is Hausdorff iff the diagonal is closed in $X^2$ (which proof also uses some contrapositive), and which has the advantage of working in any space, $T_1$ or not, and not using nets (as some proofs do).