Translating proofs from an impredicative type system to a predicative one

Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the…