proposition: Theorem isapropisisolated (X : UU) (x : X) : isaprop (isisolated X x).
proof: Proof. intros. apply isofhlevelsn. intro is. apply impred. intro x'. apply (isapropdec _ (isaproppathsfromisolated X x is x')). Defined.
imports: UniMath.Foundations.PartC