The type theory P corresponds to the logical framework LF. In this paper we present H, a variant of P where convertibility is not implemented by means of the customary conversion rule, but instead type conversions are made explicit in the terms. This means that the time to type check a H term is proportional to the size of the term itself. We define an erasure map from H to P, and show that through this map the type theory H corresponds exactly to P: any H judgment will be erased to a P judgment, and conversely each P judgment can be lifted to a H judgment. We also show a version of subject reduction: if two H terms are provably convertible then their types are also provably convertible.