graph_succ_equiv_inr@{} : f (inr tt) = inr tt. Proof. apply (graph_succ_top_unique (f (inr tt))). intros x. rewrite <- (eisretr f x). apply (fst (e (f^-1 x) (inr tt))). apply graph_succ_top. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.