apD_compose' {A A' : Type} {B : A' -> Type} (g : A -> A') (f : forall a, B a) {x y : A} (p : x = y) : apD f (ap g p) = (transport_compose B _ _ _)^ @ apD (f o g) p. Proof. by destruct p. Defined.
Require Import Basics.Overture Basics.Tactics.