in_N@{p} (n : Graph) := forall (P : Graph -> Type@{p}), (forall A, IsHProp (P A)) -> P graph_zero -> (forall A, P A -> P (graph_succ A)) -> P n.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.