X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fmap_iter_p.ma;h=7550d89b2359a863d49ad7c0608d3aebe4f37636;hb=f57cdba1f7cad1891a2fcc38432f73a584d47e48;hp=ff48d4d061141c9f7a84bf642e04c7aa55ac2408;hpb=0f67d865f8fa608397c9cd5d534c51e7f1e4ae55;p=helm.git

diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma
index ff48d4d06..7550d89b2 100644
--- a/helm/software/matita/library/nat/map_iter_p.ma
+++ b/helm/software/matita/library/nat/map_iter_p.ma
@@ -267,7 +267,7 @@ elim k 3
          apply le_S.
          assumption
         ]
-      |apply H2[autobatch|apply le_n]
+      |apply H2[autobatch |apply le_n]
       ]
     ]
   ]
@@ -325,13 +325,13 @@ apply (nat_case n)
            apply lt_to_not_eq.
            apply (le_to_lt_to_lt ? m)
             [apply (trans_le ? (m-k))
-              [assumption|autobatch]
+              [assumption| autobatch]
             |apply le_S.apply le_n
             ]
           ]
         |apply not_eq_to_eqb_false.
          apply lt_to_not_eq.
-         unfold.autobatch
+         unfold. autobatch;
         ]
       ]
     |apply le_S_S_to_le.assumption
@@ -362,7 +362,7 @@ elim n 2
        ]
      |apply sym_eq.
        apply plus_to_minus.
-       autobatch.
+       autobatch;
      ]
    |intros.
      cut ((S n1) \neq k1)