succ@{} : N -> N. Proof. intros [n nrec]. exists (graph_succ n). intros P PH P0 Ps. apply Ps. exact (nrec P PH P0 Ps). Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.