proposition: Lemma isapropifcontr {X : UU} (is : iscontr X) : isaprop X.
proof: 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.
imports: UniMath.Foundations.PartA