proposition: Theorem eh_V {X} {a : X} (p q : idpath (idpath a) = idpath (idpath a)) : eh p q @ eh q p = 1.
proof: 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.
imports: HoTT(Basics Types)