ap_snd_path_prod' {A B : Type} {x x' : A} {y y' : B} (p : x = x') (q : y = y') : ap snd (path_prod' p q) = q. Proof. apply ap_snd_path_prod. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.