updating the structures for sorts

[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 080f9a45fb883fc573d8945af970b0216c4d726c..7550d89b2359a863d49ad7c0608d3aebe4f37636 100644 (file)
--- a/helm/software/matita/library/nat/map_iter_p.ma
+++ b/helm/software/matita/library/nat/map_iter_p.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/map_iter_p.ma".
-
 include "nat/permutation.ma".
 include "nat/count.ma".
 
@@ -194,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
           ]   
         ]
@@ -269,7 +267,7 @@ elim k 3
          apply le_S.
          assumption
         ]
-      |apply H2[autobatch|apply le_n]
+      |apply H2[autobatch |apply le_n]
       ]
     ]
   ]
@@ -327,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
@@ -364,7 +362,7 @@ elim n 2
        ]
      |apply sym_eq.
        apply plus_to_minus.
-       autobatch.
+       autobatch;
      ]
    |intros.
      cut ((S n1) \neq k1)