{X} (P : X -> Type) (f : forall x, P x) {x1 x2 : X} (p : x1 = x2) : ap (transport P p) (apD f p^) @ apD f p = transport_pV P p (f x2). Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.