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=68dbcd02022874a025a9444aa1125b0458816fbb;hp=0d3bac82c6572b33eca87f3c2dfdf6626280a9c5;hpb=c445ba5534cccde19016c92660ab52777af221c0;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 0d3bac82c..7550d89b2 100644
--- a/helm/software/matita/library/nat/map_iter_p.ma
+++ b/helm/software/matita/library/nat/map_iter_p.ma
@@ -192,7 +192,7 @@ split
          apply H5
           [rewrite < H8.assumption
           |apply le_n
-          |unfold.intro.rewrite > H8 in H2.
+          |unfold.intro.
            apply (not_le_Sn_n n).rewrite < H9.assumption
           ]   
         ]
@@ -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)