From 95b46b9d1d914a41328bab8e543d336556714a74 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Nov 2005 09:05:54 +0000 Subject: [PATCH] Last details. --- helm/matita/library/list/sort.ma | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) 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 -- 2.39.2