{X} {a : X} {u v : idpath a = idpath a} (p : u = v) : (ehrnat p 1 [I] ulnat p) @ whiskerR (eh_p1 u) _ = whiskerL _ (eh_p1 v) @ urnat p. Proof. destruct p. apply lrucancel_sHs_1_pp. Defined.
From HoTT Require Import Basics Types.