{A : Type} {x y z : A} {p p' : x = y} {q q' : y = z} (g : p = p') (h k : q = q') : (g @@ h = g @@ k) -> (h = k). Proof. intro r. induction g, p, q. refine ((whiskerL_1p h)^ @ _). refine (_ @ (whiskerL_1p k)). refine (whiskerR _ _). refine (whiskerL _ _). apply r. Defined.
Require Import Basics.Overture Basics.Tactics.