Translating Proofs from an Impredicative Type System to a Predicative One. - Thiago Felicissimo; Frédéric Blanqui; Ashish Kumar Barnawal (CSL, 2023)