graph_succ_not_top@{} {A : Graph} (x : vert A) : ~(edge (graph_succ A) (inr tt) (inl x)) := idmap.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.