Moved [equiv_rect] and [equiv_intro] from [types/Record.v] to [Equivalences.v].