one@{} : N. Proof. exists graph_one. intros P PH P0 Ps. rewrite <- graph_succ_zero. apply Ps, P0. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.