Theorem isweqrecompl_ne' (X : UU) (x : X) (is : isisolated X x) (neq_x : neqPred x) : isweq (recompl_ne _ x neq_x). Proof. intros. set (f := recompl_ne X x neq_x). intro y. unfold neqPred,negProp in neq_x; unfold isisolated in is. apply (iscontrweqb (weqtotal2overcoprod _)). induction (is y) as [eq|ne]. {induction eq. refine (iscontrweqf (weqii2withneg _ _) _). {intros z; induction z as [z e]; induction z as [z neq]; simpl in *. contradicts (!e) (negProp_to_neg neq). } {change x with (f (ii2 tt)). simple refine ((_,,_),,_). {exact tt. } {apply idpath. } {intro w. induction w as [t e]. unfold f in *; simpl in *. induction t. apply maponpaths. apply isaproppathsfromisolated. exact is. }}} {refine (iscontrweqf (weqii1withneg _ _) _). {intros z; induction z as [z e]; simpl in *. contradicts ne e. } {simple refine ((_,,_),,_). {exists y. apply neg_to_negProp. assumption. } {simpl. apply idpath. } intros z; induction z as [z e]; induction z as [z neq]; induction e; simpl in *. induction (proofirrelevance _ (pr1 (pr2 (neq_x z))) neq (neg_to_negProp ne)). apply idpath. }} Defined.