{A B : Type} {g : A -> B} {y1 y2 : A} {x : B} (p : y1 = y2) (q : x = g y1) : transport (fun y => x = g y) p q = q @ (ap g p). Proof. destruct p. symmetry; apply concat_p1. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.