Lemma pathsfuntransposoft1 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t1) t2. Proof. intros. unfold funtranspos. rewrite (pathsrecomplfxtoy t1 t2 is1 _). apply idpath. Defined.