resize_nrec@{p0 p1} (n : Graph) (nrec : in_N@{p0} n) : in_N@{p1} n. Proof. intros P' PH' P0' Ps'. srefine ((equiv_smalltype (P' n)) (nrec (fun A => smalltype (P' A)) _ _ _)); try exact _; cbn. - exact ((equiv_smalltype (P' graph_zero))^-1 P0'). - intros A P'A. exact ((equiv_smalltype (P' (graph_succ A)))^-1 (Ps' A ((equiv_smalltype (P' A)) P'A))). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.