proposition: Lemma transport_path_prod_uncurried {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: Proof. destruct x, y, H; simpl in *. path_induction. reflexivity. Defined.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty