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