succ_inj@{} (n m : N) (p : succ n = succ m) : n = m. Proof. apply path_N. apply ((graph_succ_path_equiv n.1 m.1)^-1). exact (p..1). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.