{A : Type} {P : A -> Type} {x x' : A} {y : P x} {y' : P x'} (p : x = x') (q : DPath P p y y') : ap pr1 (path_sigma_dp (p; q)) = p. Proof. apply ap_pr1_path_sigma. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.