Lemma hNatRecursionUniq (P:nat->Type) (p0:P 0) (IH:∏ n, P n->P(S n)) : ∃! (f:∏ n, P n), f 0=p0 × ∏ n, f(S n) = IH n (f n). Proof. intros. exact (iscontrweqf (helper_C _ _ _) (iscontrcoconustot _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.