Lemma isapropifcontr {X : UU} (is : iscontr X) : isaprop X. Proof. intros. set (f := λ x : X, tt). assert (isw : isweq f) by (apply isweqcontrtounit; assumption). apply (isofhlevelweqb (S O) (make_weq f isw)). intros x x'. apply iscontrpathsinunit. Defined.