Theorem isaproppathstoisolated (X : UU) (x : X) (is : isisolated X x) : ∏ x' : X, isaprop (x' = x). Proof. intros. apply (isofhlevelweqf 1 (weqpathsinv0 x x') (isaproppathsfromisolated X x is x')). Defined.