Lemma helper_B (P:nat->Type) (p0:P 0) (IH:∏ n, P n->P(S n)) (f:∏ n, P n) : weq (f = nat_rect P p0 IH) ((f 0=p0) × (∏ n, f(S n)=IH n (f n))). Proof. intros. exact (weqcomp (weqtoforallpaths _ _ _) (helper_A _ _ _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.