N_rec_beta_succ'@{} (n : N) : N_rec' (succ n) = xs (N_rec' n). Proof. unfold N_rec'. refine (_ @ snd (pf (succ n)).2 (n ; N_lt_succ n) @ _). - apply ap, path_sigma_hprop; reflexivity. - apply ap. transitivity ((partial_Nrec_restr n (pf (succ n))).1 (refl_seg n)). + refine (ap (pf (succ n)).1 _). apply path_sigma_hprop; reflexivity. + apply ap10@{p x nr}. apply ap, path_contr. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.