graph_add_succ@{} (A B : Graph) : graph_add A (graph_succ B) = graph_succ (graph_add A B). Proof. apply equiv_path_graph. exists (equiv_inverse (equiv_sum_assoc (vert A) (vert B) Unit)). intros [x|[x|[]]] [y|[y|[]]];apply iff_reflexive@{u s}. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.