ap_pr1_path_contr_basedpaths' {X : Type} {x y z : X} (p : y = x) (q : z = x) : ap pr1 (path_contr ((y;p) : {y':X & y' = x}) (z;q)) = p @ q^. Proof. destruct p, q; reflexivity. Defined.
Require Import Overture PathGroupoids.