fact: Definition weqleFtototalwithnat { T : UU } (F : T -> T) (t t' : T) : weq (leF F t t') (total2 (λ n : nat, (iteration F n t) = t')) := make_weq _ (isweqleFtototal2withnat F t t').
imports: UniMath.Foundations.NaturalNumbers