{X} {a : X} {u v w : idpath a = idpath a} (p : 1 = w) (q : u = 1) (r : 1 = v) : Wlrnat_V_p_pp (ehrnat_pp q r _) (ehrnat_pp q r _) (wlrnat_p_pp p q r) (wlrnat_pp_p q r p) (wlrnat_V p q) (wlrnat_V p r) = wlrnat_V p (q @ r). Proof. revert u q. snrapply (equiv_path_ind (equiv_path_inverse _)). by destruct p, r. Defined.
From HoTT Require Import Basics Types.