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