graph_succ_top@{} {A : Graph} (x : vert (graph_succ A)) : edge (graph_succ A) x (inr tt). Proof. destruct x as [x|x]; exact tt. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.