  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 challenges in this domain is to translate proofs
written in proof assistants based on impredicative logics to proof assistants
based on predicative logics, whenever impredicativity is not used in an
essential way.
  In this paper we present a transformation for sharing proofs with a core
predicative system supporting prenex universe polymorphism (like in Agda). It
consists in trying to elaborate each term into a predicative universe
polymorphic term as general as possible. The use of universe polymorphism is
justified by the fact that mapping each universe to a fixed one in the target
theory is not sufficient in most cases. During the elaboration, we need to
solve unification problems in the equational theory of universe levels. In
order to do this, we give a complete characterization of when a single equation
admits a most general unifier. This characterization is then employed in a
partial algorithm which uses a constraint-postponement strategy for trying to
solve unification problems.
  The proposed translation is of course partial, but in practice allows one to
translate many proofs that do not use impredicativity in an essential way.
Indeed, it was implemented in the tool Predicativize and then used to translate
semi-automatically many non-trivial developments from Matita's library to Agda,
including proofs of Bertrand's Postulate and Fermat's Little Theorem, which (as
far as we know) were not available in Agda yet.
