{A : Type} {x y : A} (p : x = y) (q : idpath x = idpath x) (r : idpath y = idpath y) : (concat_1p p)^ @ whiskerR q p @ concat_1p p = (concat_p1 p)^ @ whiskerL p r @ concat_p1 p <~> transport (fun a => idpath a = idpath a) p q = r. Proof. destruct p. simpl. refine (_ oE (equiv_whiskerR _ _ 1)^-1). refine (_ oE (equiv_whiskerL 1 _ _)^-1). refine (equiv_concat_lr _ _). - symmetry; apply whiskerR_p1_1. - apply whiskerL_1p_1. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.