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