{A B : Type} (z z' : A * B) : (fst z = fst z') * (snd z = snd z') <~> (z = z') := Build_Equiv _ _ (path_prod_uncurried z z') _.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.