+lemma insert_ind :
+ ∀A:Set. ∀le: A → A → bool. ∀x.
+ ∀P:(list A → list A → Prop).
+ ∀H:(∀l: list A. l=[] → P [] [x]).
+ ∀H2:
+ (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+ le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
+ ∀H3:
+ (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+ le x he = true → l=he::l' → P (he::l') (x::he::l')).
+ ∀l:list A. P l (insert ? le x l).
+ intros.
+ apply (
+ let rec insert_ind (l: list A) \def
+ match l in list
+ return
+ λli.
+ l = li → P li (insert ? le x li)
+ with
+ [ nil ⇒ H l
+ | (cons he l') ⇒
+ match le x he
+ return
+ λb. le x he = b → l = he::l' →
+ P (he::l')
+ (match b with
+ [ true ⇒ x::he::l'
+ | false ⇒ he::(insert ? le x l') ])
+ with
+ [ true ⇒ H2 l he l' (insert_ind l')
+ | false ⇒ H1 l he l' (insert_ind l')
+ ]
+ (refl_eq ? (le x he))
+ ] (refl_eq ? l) in insert_ind l).
+qed.
+
+