N_rec_beta_zero'@{} : N_rec' zero = x0. Proof. refine (_ @ fst (pf zero).2). unfold N_rec'. apply ap, path_sigma_hprop; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.