Theorem isweqrecompl' (X : UU) (x : X) (is : isisolated X x) : isweq (recompl _ x). Proof. intros. set (neq_x := λ y, make_neqProp x y). apply (isweqhomot (weqrecompl_ne X x is neq_x ∘ weqcoprodf (compl_ne_weq_compl X x neq_x) (idweq unit))%weq). {intro y. induction y as [y|t]; apply idpath. } apply weqproperty. Defined.