proposition: 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: Proof. intros. exact (iscontrweqf (helper_C _ _ _) (iscontrcoconustot _ _)). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA