Type@{nr} := sig@{nr nr} (fun f : N -> X => prod@{x nr} (f zero = x0) (forall m:N, f (succ m) = xs (f m))). Local nrec_partials@{} : -> partials. Proof. intros f n. exists (fun mh => f.1 mh.1). split. - exact (fst f.2). - intros mh. exact (snd f.2 mh.1). Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.