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