Some stylistic preferences in Prod.v

Do you prefer the `destruct p. destruct q.` form over the `destruct p, q.` form?  (The latter is shorter, but I otherwise don't care.)