Definition prodtosecovercoprod {X Y : UU} (P : X ⨿ Y -> UU) (a : (∏ x, P (ii1 x)) × (∏ y : Y, P (ii2 y))) : ∏ xy : X ⨿ Y, P xy. Proof. intros. induction xy as [ x | y ]. - exact (pr1 a x). - exact (pr2 a y). Defined.