-(*
-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.
-*)