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