Theorem isdecpropfibseq1 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) : isdecprop X -> isaprop Z -> isdecprop Y. Proof. intros isx isz. assert (isc : iscontr Z) by apply (iscontraprop1 isz z). assert (X0 : isweq f) by apply (isweqfinfibseq f g z fs isc). apply (isdecpropweqf (make_weq _ X0) isx). Defined.