graph_succ_top_unique@{} {A : Graph} (y : vert (graph_succ A)) (yt : forall x, edge (graph_succ A) x y) : y = inr tt. Proof. destruct y as [y|[]]. - destruct (yt (inr tt)). - reflexivity. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.