{A : Type} {B : A -> Type} {f g : forall x, B x} (p : forall x, f x = g x) {x y : A} (q : x = y) : apD f q = ap (transport B q) (p x) @ apD g q @ (p y)^. Proof. apply moveL_pV. destruct q; unfold apD, transport. symmetry. exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^). Defined.
Require Import Basics.Overture Basics.Tactics.