Heterogeneous equality helper lemmas

This file contains small HEq lemmas that belong in Mathlib rather than in domain-specific developments.

theorem Prod.mk_heq {α : Type u} {β β' : Type v} {a : α} {b : β} {b' : β'} (h : b ≍ b') : (a, b) ≍ (a, b')

Build a heterogeneous equality between pairs with the same first component from a heterogeneous equality between their second components.