**Yes;** this is given in Mines, Richman, Ruitenburg, *A course in constructive algebra*, on p.54, stated just before Lemma 4.1, and proved in that lemma by a Church-Rosser argument.  (Thanks to Thierry Coquand for pointing me to this proof.)