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