proposition: Theorem eh_p_pp {X} {a : X} (p q r : idpath a = idpath a) : eh p (q @ r) @ (concat_pp_p _ _ _ @ whiskerL _ (eh p r)^) = concat_p_pp _ _ _ @ whiskerR (eh p q) _ @ concat_pp_p _ _ _.
proof: Proof. nrapply eh_p_pp_gen. - exact (urnat_pp q r). - exact (urnat_pp q r). - exact (wlrnat_p_pp p q r). Defined.
imports: HoTT(Basics Types)