Definition isisolated_ne_to_isisolated {X x neq_x} : isisolated_ne X x neq_x -> isisolated X x. Proof. intros i y. induction (i y) as [eq|ne]. - exact (ii1 eq). - apply ii2. use negProp_to_neg. + exact (neq_x y). + exact ne. Defined.