Reinstated [equiv_rect], [equiv_intro], accidentally deleted when rebasing.