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