Lemma isweqleFtototal2withnat {T : UU} (F : T -> T) (t t' : T) : isweq (leFtototal2withnat F t t'). Proof. intros. set (f := leFtototal2withnat F t t'). set (g := total2withnattoleF F t t'). assert (egf : ∏ x : _, paths (g (f x)) x). { intro x. induction x as [ | y H0 IHH0 ]. - apply idpath. - simpl. simpl in IHH0. destruct (leFtototal2withnat F t y H0) as [ m e ]. destruct e. simpl. simpl in IHH0. apply (@maponpaths _ _ (leF_S F t (iteration F m t)) _ _ IHH0). } assert (efg : ∏ x : _, paths (f (g x)) x). { intro x. destruct x as [ n e ]. destruct e. simpl. apply leFtototal2withnat_l0. } apply (isweq_iso _ _ egf efg). Defined.