{A} {x y z : A} {p p' p'' : x = y} (q : y = z) (r : p = p') (s : p' = p'') : whiskerR (r @ s) q = whiskerR r q @ whiskerR s q. Proof. destruct q, r, s; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.