{A : Type} {x1 x2 : A} (p : x1 = x2) (q : x1 = x1) : transport (fun x => x = x) p q = p^ @ q @ p. Proof. destruct p; simpl. exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.