The statement that if $R$ is Jacobson (i.e., $\mathrm{J}(R/I)\subseteq\mathrm{Nil}(R/I)$ for every ideal $I$ of $R$) then so is $R[X]$ is constructively provable. The proof is in this preprint of mine.
> [A constructive proof of general Nullstellensatz for Jacobson rings][1], arXiv:2406.06078 [math.AC]

The proof is the same as the classical one in [Matthew Emerton's PDF][2]. You can eliminate the use of prime ideals and maximal ideals by using the idea of entailment relations. See [Peter Schuster and Daniel Wessel, Syntax for Semantics: Krull’s Maximal Ideal Theorem][3] for details.

[1]:https://arxiv.org/abs/2406.06078
[2]:https://www.math.uchicago.edu/~emerton/pdffiles/jacobson.pdf
[3]:https://link.springer.com/chapter/10.1007/978-3-030-65824-3_6