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