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