Lemma leFtototal2withnat_l0 {T : UU} (F : T -> T) (t : T) (n : nat) : (leFtototal2withnat F t _ (leFiter F t n)) = (tpair _ n (idpath (iteration F n t))). Proof. intros. induction n as [ | n IHn ]. - apply idpath. - simpl. set (h := fun ne : total2 (λ n0 : nat, paths (iteration F n0 t) (iteration F n t)) => tpair (λ n0 : nat, paths (iteration F n0 t) (iteration F (S n) t)) (S (pr1 ne)) (maponpaths F (pr2 ne))). apply (@maponpaths _ _ h _ _ IHn). Defined.