graph_add_one_succ@{} (A : Graph) : graph_add A graph_one = graph_succ A. Proof. apply equiv_path_graph. exists equiv_idmap. intros [x|[]] [y|[]]; apply iff_reflexive@{u s}. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.