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