  Many automatic theorem provers are restricted to untyped logics, and existing
translations from typed logics are bulky or unsound. Recent research proposes
monotonicity as a means to remove some clutter when translating monomorphic to
untyped first-order logic. Here we pursue this approach systematically,
analysing formally a variety of encodings that further improve on efficiency
while retaining soundness and completeness. We extend the approach to rank-1
polymorphism and present alternative schemes that lighten the translation of
polymorphic symbols based on the novel notion of "cover". The new encodings are
implemented in Isabelle/HOL as part of the Sledgehammer tool. We include
informal proofs of soundness and correctness, and have formalised the
monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new
encodings vastly superior to previous schemes.
