graph_add_zero_r@{} (A : Graph) : graph_add A graph_zero = A. Proof. apply equiv_path_graph. exists (sum_empty_r (vert A)). intros [x|[]] [y|[]]. apply iff_reflexive@{u s}. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.