path_prod' {A B : Type} {x x' : A} {y y' : B} : (x = x') -> (y = y') -> ((x,y) = (x',y')) := fun p q => path_prod (x,y) (x',y') p q.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.