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