proposition: Lemma hNatRecursion_weq (P:nat->Type) (IH:∏ n, P n->P(S n)) : weq (total2 (fun f:∏ n, P n => ∏ n, f(S n)=IH n (f n))) (P 0).
proof: Proof. intros. exists (λ f, pr1 f 0). intro p0. apply (iscontrweqf (helper_D _ _ _)). apply hNatRecursionUniq. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA