proposition: Lemma isdecproppathsfromisolated (X : UU) (x : X) (is : isisolated X x) (x' : X) : isdecprop (x = x').
proof: Proof. intros. apply isdecpropif. - apply isaproppathsfromisolated. assumption. - apply (is x'). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom