Definition rdistrtoprod (X Y Z : UU) : (X × Y) ⨿ (X × Z) -> X × (Y ⨿ Z). Proof. intros X0. induction X0 as [ d | d ]. induction d as [ t x ]. apply (make_dirprod t (ii1 x)). induction d as [ t x ]. apply (make_dirprod t (ii2 x)). Defined.