Lemma isdecpropif' (X : UU) : isaprop X -> X ⨿ ¬ X -> iscontr (X ⨿ ¬ X). Proof. intros is a. assert (is1 : isaprop (coprod X (neg X))) by (apply isapropdec; assumption). apply (iscontraprop1 is1 a). Defined.