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