Record types are an important tool for programming and dependent record types are proven to be very useful for program specification and verification. Unfortunately all known embedding of the dependent record type in the type theory had some imperfections. In this paper we present a new type constructor, dependent intersection that allows us to define records that combine the most advantages of previously known approaches, while avoiding most of their disadvantages.