Definition foralltototal {X : UU} (P : X -> UU) (PP : ∏ x, P x -> UU) : (∏ x, ∑ p, PP x p) -> (∑ (s0 : ∏ x, P x), ∏ x, PP x (s0 x)). Proof. intros X0. exists (λ x, pr1 (X0 x)). apply (λ x, pr2 (X0 x)). Defined.