{A B} (P : A * B -> Type) {x y : A * B} (H : (fst x = fst y) * (snd x = snd y)) (Px : P x) : transport P (path_prod_uncurried _ _ H) Px = transport (fun x => P (x, snd y)) (fst H) (transport (fun y => P (fst x, y)) (snd H) Px). Proof. destruct x, y, H; simpl in *. path_induction. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.