graph_zero_neq_succ@{} {A : Graph} : graph_zero <> graph_succ A. Proof. intros p. destruct ((equiv_path_graph graph_zero (graph_succ A))^-1 p) as [f e]. exact (f^-1 (inr tt)). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.