Definition tototal2overcoprod {X Y : UU} (P : X ⨿ Y -> UU) (xpyp : coprod (∑ x : X, P (ii1 x)) (∑ y : Y, P (ii2 y))) : total2 P. Proof. intros. induction xpyp as [ xp | yp ]. induction xp as [ x p ]. apply (tpair P (ii1 x) p). induction yp as [ y p ]. apply (tpair P (ii2 y) p). Defined.