{A B : Type} (z z' : A * B) (pq : (fst z = fst z') * (snd z = snd z')) : (z = z'). Proof. change ((fst z, snd z) = (fst z', snd z')). case (fst pq). case (snd pq). reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.