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