X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Farith_2a.ma;h=92224c4c9560d1f51b5c54e52c144fda38b2ec00;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=b5ff26116ef36e2b41f8e3c4abd9a51fc374f45c;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
index b5ff26116..92224c4c9 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
@@ -87,7 +87,7 @@ lemma lt_plus_SO_to_le: ∀x,y. x < y + (𝟏) → x ≤ y.
 
 (* Iterators ****************************************************************)
 
-lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+𝟏) b = f (f^l b).
+lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. (f^(l+𝟏)) b = f ((f^l) b).
 #B #f #b #l
 <niter_succ //
 qed.