{A : Type} {x y1 y2 : A} (p : y1 = y2) (q : x = y1) (r : x = y2) : q @ p = r <~> transport (fun y => x = y) p q = r. Proof. destruct p; simpl. exact (equiv_concat_l (concat_p1 q)^ r). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.