{A} {P : A -> Type} (f : forall x, P x) {x y z : A} (p : x = y) (q : y = z) : apD f (p @ q) = transport_pp P p q (f x) @ ap (transport P q) (apD f p) @ apD f q. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.