Lemma isdecproppathstoisolated (X : UU) (x : X) (is : isisolated X x) (x' : X) : isdecprop (x' = x). Proof. intros. apply (isdecpropweqf (weqpathsinv0 x x') (isdecproppathsfromisolated X x is x')). Defined.