...

[helm.git] / helm / software / matita / library / nat / map_iter_p.ma

diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma
index ff48d4d061141c9f7a84bf642e04c7aa55ac2408..7550d89b2359a863d49ad7c0608d3aebe4f37636 100644 (file)
--- 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)