{X} {a : X} (p q : idpath (idpath a) = idpath (idpath a)) : eh p q @ eh q p = 1. Proof. nrapply eh_V_gen. - exact (ehlnat_1p p). - exact (ehlnat_1p p). - exact (ehrnat_p1 q). - exact (ehrnat_p1 q). - exact (wlrnat_V p q). Defined.
From HoTT Require Import Basics Types.