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