{A} {w x y z : A} (p : w = x) {q q' : x = y} (h : q = q') (r : y = z) : whiskerL p (whiskerR h r) @ concat_p_pp p q' r = concat_p_pp p q r @ whiskerR (whiskerL p h) r. Proof. by destruct h, p, q, r. Defined.
Require Import Basics.Overture Basics.Tactics.