{A : Type} {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z) : whiskerL p (concat_p_pp q r s) @ concat_p_pp p (q@r) s @ whiskerR (concat_p_pp p q r) s = concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s. Proof. case p, q, r, s. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.