Last details.

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index e620ed5369d3eefaa3c387a87e0fe5c12ec54693..939cecedec6486a27274a4ce6ac834888f7c58ce 100644 (file)
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -95,10 +95,8 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
   ].
 
 lemma ordered_injective:
-  ∀ A:Set. ∀ le:A → A → bool.
-  ∀ l:list A.
-  ordered A le l = true
-  \to ordered A le (tail A l) = true.
+  ∀A:Set. ∀le:A → A → bool.
+   ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true.
   intros 3 (A le l).
   elim l
   [ simplify; reflexivity;
@@ -134,7 +132,7 @@ lemma insert_sorted:
     ordered A le l = true \to ordered A le (insert A le x l) = true.
  intros 5 (A le H l x).
  apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
- intros; simplify; intros;
+ clear l; intros; simplify; intros;
   [2: rewrite > H1;
     [ generalize in match (H ? ? H2); clear H2; intro;
       generalize in match H4; clear H4;
@@ -168,7 +166,7 @@ theorem insertionsort_sorted:
   elim l;
   [ simplify;
     reflexivity;
-  | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
+  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
     assumption;
   ]
 qed.
\ No newline at end of file