{X} {a : X} {u v : idpath a = idpath a} (p : u = 1) (q : 1 = v) (w : idpath a = idpath a) : (ehrnat p w [-] ehrnat q w) @ whiskerL _ (whiskerL_pp _ p q)^ = (whiskerR (whiskerR_pp _ p q)^ _) @ ehrnat (p @ q) w. Proof. revert u p. snrapply (equiv_path_ind (equiv_path_inverse _)). destruct q. cbn. apply rlucancel, lrucancel_sVs_1. Defined.
From HoTT Require Import Basics Types.