Lemma isdecpropfromdecincl {X Y : UU} (f : X -> Y) : isdecincl f -> isdecprop Y -> isdecprop X. Proof. intros isf isy. induction (pr1 isy) as [ y | n ]. - assert (w : weq (hfiber f y) X) by apply (weqhfibertocontr f y (iscontraprop1 (isdecproptoisaprop _ isy) y)). apply (isdecpropweqf w (isf y)). - apply isdecpropif. apply (isapropinclb _ isf isy). apply (ii2 (negf f n)). Defined.