{A B} (P : A * B -> Type) {x y : A * B} (HA : fst x = fst y) (HB : snd x = snd y) (Px : P x) : transport P (path_prod _ _ HA HB) Px = transport (fun x => P (x, snd y)) HA (transport (fun y => P (fst x, y)) HB Px) := transport_path_prod_uncurried P (HA, HB) Px.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.