N_zero_or_succ@{} (n : N) : (n = zero) + { m : N & n = succ m }. Proof. apply (functor_sum (path_N _ _) (functor_sigma (Q := fun m:N => n = succ m) idmap (fun m => path_N _ (succ m)))). destruct n as [n nrec]; cbn. srefine (resize_nrec n nrec (fun n => (n = graph_zero) + {m : N & n = graph_succ m.1}) _ _ _); cbn. - apply inl; reflexivity. - intros A [A0|[m As]]; apply inr. + exists zero. rewrite A0. reflexivity. + exists (succ m). rewrite As. reflexivity. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.