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