Theorem isaproppathsfromisolated_ne (X : UU) (x : X) (neq_x : neqPred x) (is : isisolated_ne X x neq_x) (y : X) : isaprop (x = y). Proof. intros. unfold isisolated_ne in is. apply invproofirrelevance; intros m n. set (Q y := (x = y) ⨿ (neq_x y)). assert (a := (transport_section is m) @ !(transport_section is n)). induction (is x) as [j|k]. - assert (b := transport_map (λ y p, ii1 p : Q y) m j); simpl in b; assert (c := transport_map (λ y p, ii1 p : Q y) n j); simpl in c. assert (d := equality_by_case (!b @ a @ c)); simpl in d. rewrite 2? transportf_id1 in d. apply (pathscomp_cancel_left j). assumption. - contradicts (neq_x x k) (idpath x). Defined.