A constructive counterpart of the subdirect representation theorem for reduced rings

We give a constructive counterpart of the theorem of Andrunakievi\v{c} and Rjabuhin, which states that every reduced ring is a subdirect product of domains. As an application, we extract a constructive proof of the fact that every ring $A$ satisfying $\forall x\in A. x^3=x$ is commutative from a classical proof. We also prove a similar result for semiprime ideals.