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