Lemma isdecproppathsfromisolated (X : UU) (x : X) (is : isisolated X x) (x' : X) : isdecprop (x = x'). Proof. intros. apply isdecpropif. - apply isaproppathsfromisolated. assumption. - apply (is x'). Defined.