proposition: Lemma total2withnattoleF {T : UU} (F : T -> T) (t t' : T) (a : total2 (λ n : nat, (iteration F n t) = t')) : leF F t t'.
proof: Proof. intros. destruct a as [ n e ]. destruct e. apply leFiter. Defined.
imports: UniMath.Foundations.NaturalNumbers