{A : Type} {x1 x2 y : A} (p : x1 = x2) (q : x1 = y) : transport (fun x => x = y) p q = p^ @ q. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.