{A : Type} {P : A -> Type} {C : forall x, P x -> Type} {x1 x2 : A} (p : x1 = x2) (f : forall y : P x1, C x1 y) : (transport (fun x => forall y : P x, C x y) p f) == (fun y => transport (C x2) (transport_pV _ _ _) (transportD _ _ p _ (f (p^ # y)))) := match p with idpath => fun _ => 1 end.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids