N_propind@{P} (P : N -> Type@{P}) `{forall n, IsHProp (P n)} (P0 : P zero) (Ps : forall n, P n -> P (succ n)) : forall n, P n. Proof. intros [n nrec]. pose (Q := fun m:Graph => forall (mrec : in_N m), P (m;mrec)). refine (resize_nrec n nrec Q _ _ _ nrec); clear n nrec. - intros zrec. refine (transport P _ P0). apply ap. apply path_ishprop. - intros A QA Asrec. pose (m := (A ; pred_in_N A Asrec) : N). refine (transport P _ (Ps m (QA (pred_in_N A Asrec)))). apply path_N; reflexivity. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.