Lemma leFtototal2withnat {T : UU} (F : T -> T) (t t' : T) (a : leF F t t') : total2 (λ n : nat, (iteration F n t) = t'). Proof. intros. induction a as [ | b H0 IH0 ]. - split with O. apply idpath. - split with (S (pr1 IH0)). simpl. apply (@maponpaths _ _ F (iteration F (pr1 IH0) t) b). apply (pr2 IH0). Defined.