Theorem isaproppathsfromisolated (X : UU) (x : X) (is : isisolated X x) : ∏ x', isaprop(x = x'). Proof. intros. apply iscontraprop1inv. intro e. induction e. set (f := λ e : x = x, coconusfromtpair _ e). assert (is' : isweq f) by apply (onefiber (λ x' : X, x = x') (x : X) (λ x' : X, is x')). assert (is2 : iscontr (coconusfromt _ x)) by apply iscontrcoconusfromt. apply (iscontrweqb (make_weq f is')). assumption. Defined.