{A : Type} {x y z : A} (p : x = y) (q : y = z) : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q = whiskerL p (concat_1p q). Proof. case p, q. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.