Lemma pathsinvcuntonweqoft {T : UU} (t : T) (is : isisolated T t) (t'w : isolated T × (compl T t ≃ compl T t)) : invcutonweq t is t'w t = pr1 (pr1 t'w). Proof. intros. unfold invcutonweq. simpl. unfold recompl. unfold coprodf. unfold invmap. simpl. unfold invrecompl. induction (is t) as [ ett | nett ]. - apply pathsfuntransposoft1. - induction (nett (idpath _)). Defined.