graph_succ@{} (A : Graph) : Graph. Proof. srefine (Build_Graph (sum@{s s} (vert A) Unit) _ _). - intros [x|x] [y|y]. + exact (edge A x y). + exact Unit. + exact Empty. + exact Unit. - cbn; intros [x|x] [y|y]; exact _. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.