The Lean proof assistant features a typechecker kernel that makes use of a set of “definitional equalities” for identifying terms under certain syntactic and typing conditions. While providing for convenient formalization, some definitional equalities in particular complicate meta-theoretical analyses and the export of Lean proofs to other proof assistants via logical frameworks such as Dedukti. In this paper, we describe a translation from Lean to a smaller theory “ \(\text {Lean}^-\) ” with fewer such definitional equalities, specifically eliminating uses of proof irrelevance and “K-like reduction” in the typing of Lean terms. We adapt a general translation from extensional to intensional type theory, making Lean’s implicit use of these definitional equalities explicit through the use of type casts and a corresponding proof irrelevance axiom. The translation has been implemented in Lean itself in a tool called Lean4Less ( https://github.com/rish987/Lean4Less ), which is able to successfully translate certain libraries (e.g. the Lean standard library) to \(\text {Lean}^-\) . The methods developed for this translation may also be transferrable to other proof assistants based on dependent type theory.