{A : Type} {B : A -> Type} {f g : forall a, B a} {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1) : transport (fun x => f x = g x) p q = (apD f p)^ @ ap (transport B p) q @ (apD g p). Proof. destruct p; simpl. exact ((ap_idmap _)^ @ (concat_1p _)^ @ (concat_p1 _)^). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.