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