From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Nov 2005 09:05:54 +0000 (+0000)
Subject: Last details.
X-Git-Tag: V_0_7_2_3~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=95b46b9d1d914a41328bab8e543d336556714a74

Last details.
---

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index e620ed536..939cecede 100644
--- 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