graph_succ_zero@{} : graph_succ graph_zero = graph_one. Proof. rewrite <- graph_add_one_succ. apply graph_add_zero_l. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.