Lemma total2asstol {X : UU} (P : X -> UU) (Q : total2 P -> UU) : (∑ x : X, ∑ p : P x, Q (tpair P x p)) -> total2 Q. Proof. intros xpq. use tpair. - use tpair. + apply (pr1 xpq). + apply (pr1 (pr2 xpq)). - exact (pr2 (pr2 xpq)). Defined.