{A A'} B {x x' : A} (C : forall x : A', B x -> Type) (f : A -> A') (p : x = x') y (z : C (f x) y) : transportD (B o f) (C oD f) p y z = transport (C (f x')) (transport_compose B f p y)^ (transportD B C (ap f p) y z). Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.