- apply (
- let rec insert_ind (l: list A) \def
- match l in list
- return
- λli.
- l = li → ordered ? le li = true →
- ordered ? le (insert A le x li) = true
- with
- [ nil ⇒ (? : l = [] → ordered ? le [] = true → ordered ? le [x] = true)
- | (cons he l') ⇒
- match le x he
- return
- λb. le x he = b → l = he::l' →
- ordered ? le (he::l') = true → ordered ? le
- (match b with
- [ 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)
- ]
- (refl_eq ? (le x he))
- ] (refl_eq ? l) in insert_ind l);
-
- intros; simplify;
- [ rewrite > insert_ind;
- [ generalize in match (H ? ? H1); clear H1; intro;
- generalize in match H3; clear H3;
+ apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
+ clear l; intros; simplify; intros;
+ [2: rewrite > H1;
+ [ generalize in match (H ? ? H2); clear H2; intro;
+ generalize in match H4; clear H4;