Some stylistic preferences in Prod.v

Why like this, rather than `case pq.2; case pq.1` (`destruct` would probably also work)?