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