{X} {a : X} {u v x y : idpath a = idpath a} p q : whiskerR (wlrnat p q) (eh v y) @ (ehrnat q x [-] ehlnat v p) = (ehlnat u p [-] ehrnat q y) @ whiskerL (eh u x) (wlrnat q p)^. Proof. destruct p, q. exact (lrucancel 1). Defined.
From HoTT Require Import Basics Types.