{A B : Type} {z z' : A * B} (p : fst z = fst z') (q : snd z = snd z') : ap snd (path_prod _ _ p q) = q. Proof. change z with (fst z, snd z). change z' with (fst z', snd z'). destruct p, q. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.