{A B : Type} (f : A -> B) (P : B -> Type) {x y : A} (p : x = y) (g : forall b:B, P b) : apD (g o f) p = (dp_compose f P p)^-1 (apD g (ap f p)) := ' f P (idpath (ap f p)) g.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.