{A} (P : A -> Type) {x y:A} (p:x=y) (z:P x) : transport_pV P p (transport P p z) = ap (transport P p) (transport_Vp P p z). Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.