A constructive counterpart of the subdirect representation theorem for reduced rings

We give a constructive counterpart of the theorem of Andrunakievič 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 $\mathrm{\forall }x\in A\mathrm{.}{x}^3=x$ is commutative from a classical proof. We also prove a similar result for semiprime ideals.