Hidden constructions in abstract algebra (6): The theorem of Maroscia and Brewer & Costa

We give a constructive deciphering for a generalization of the Quillen-Suslin theorem due to Maroscia and Brewer & Costa stating that finitely generated projective modules over R[X1,…,Xn], where R is a Prüfer domain with Krull dimension ≤1, are extended from R.