graph_unsucc_path@{} (A B : Graph) : (graph_succ A = graph_succ B) -> A = B := (graph_succ_path_equiv A B)^-1.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.