Lost of redundant typing hints removed from the functional induction term.

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 2716235d0914f0cd0a4da052a5d45b58cbc9583b..455462d8d67f823e3712a4cc587cee284da76964 100644 (file)
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -48,26 +48,6 @@ let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
        | false ⇒ he::(insert A le x l')
        ]
   ].
-(*
-theorem insert_ind:
- ∀A:Set. ∀le: A → A → bool. ∀x:A.
-  ∀P: list A → Prop.
-   ∀l:list A. P (insert A le x l).
- intros (A le x P H l).
- apply (
- let rec insert_ind (l: list A) ≝
-  match l in list return λl.P (insert A le x l) with
-   [ nil ⇒ (? : P [x])
-   | (cons he l') ⇒
-       match le x he return λb.P (match b with [ true ⇒ x::he::l' | false ⇒ he::(insert A le x l') ]) with
-        [ true ⇒ (H2 : P (x::he::l'))
-        | false ⇒ (? : P (he::(insert A le x l')))
-        ]
-   ]
- in
-  insert_ind l).
-qed.
-*)
 
 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  match l with
@@ -125,7 +105,7 @@ lemma insert_sorted:
      l = li → ordered ? le li = true →
       ordered ? le (insert A le x li) = true
   with
-   [ nil ⇒ (? : l = [] → ordered ? le [] = true → ordered ? le [x] = true)
+   [ nil ⇒ ?
    | (cons he l') ⇒
        match le x he
        return
@@ -135,18 +115,8 @@ lemma insert_sorted:
             [ true ⇒ x::he::l'
             | false ⇒ he::(insert A le x l') ]) = true
        with
-        [ true ⇒
-            (? :
-              le x he = true →
-               l = he::l' →
-                ordered ? le (he::l') = true →
-                 ordered ? le (x::he::l') = true)
-        | false ⇒
-           let res ≝ insert_ind l' in
-            (? :                  
-                  le x he = false → l = he::l' →
-                   ordered ? le (he::l') = true →
-                    ordered ? le (he::(insert ? le x l')) = true)           
+        [ true ⇒ ?
+        | false ⇒ let res ≝ insert_ind l' in ?         
         ]
        (refl_eq ? (le x he))
    ] (refl_eq ? l) in insert_ind l);