{A} B (f : forall x : A, B x) (C : forall x, B x -> Type) {x1 x2 : A} (p : x1 = x2) (z : C x1 (f x1)) : apD f p # transportD B C p _ z = transport (fun x => C x (f x)) p z. Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.