ishprop_path_N@{} (n : N) (A : Graph) : IsHProp (n.1 = A). Proof. apply ishprop_path_graph_in_N, pr2. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.