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. intros. exists (λ f, pr1 f 0). intro p0. apply (iscontrweqf (helper_D _ _ _)). apply hNatRecursionUniq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.