Yes; this is given in Mines, Richman, Ruitenberg, 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.)
Peter LeFanu Lumsdaine
- 21.3k
- 2
- 75
- 128