{A : Type} {B : A -> Type} {x y : A} {p q : x = y} (f : forall x, B x) (r : p = q) : apD f p = transport2 B r (f x) @ apD f q := match r with idpath => (concat_1p _)^ end.
Require Import Basics.Overture Basics.Tactics.