{A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') : (whiskerR a q) @ (whiskerL p' b) = (whiskerL p b) @ (whiskerR a q') := match b with idpath => match a with idpath => (concat_1p _)^ end end.
Require Import Basics.Overture Basics.Tactics.