proposition: Lemma helper_C (P:nat->Type) (p0:P 0) (IH:∏ n, P n->P(S n)) : (∑ f:∏ n, P n, f = nat_rect P p0 IH) ≃ (∑ f:∏ n, P n, f 0=p0 × ∏ n, f(S n)=IH n (f n)).
proof: Proof. intros. apply weqfibtototal. intros f. apply helper_B. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA