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