fact: Definition transport_path_prod' {A B} (P : A * B -> Type) {x y : A} {x' y' : B} (HA : x = y) (HB : x' = y') (Px : P (x,x')) : transport P (path_prod' HA HB) Px = transport (fun x => P (x, y')) HA (transport (fun y => P (x, y)) HB Px) := @transport_path_prod _ _ P (x, x') (y, y') HA HB Px.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty