- intros 5 (A le H l x).
- elim l;
- [ 2: change with (ordered A le (match le x s with
- [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true).
- apply (bool_elim ? (le x s));
- [ intros;
- change with ((le x s \land ordered A le (s::l1)) = true);
- apply andb_elim;
- rewrite > H3;
- assumption;
- | generalize in match H2;
- clear H1; clear H2;
- generalize in match s;
- clear s;
- elim l1
- [ simplify;
- rewrite > (H x a H2);
- reflexivity;
- | change with ((ordered A le (a::match le x s with
- [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true).
- apply (bool_elim ? (le x s));
- [ intros;
- change with ((le a x \land (le x s \land ordered A le (s::l2))) = true).
- apply andb_elim;
- rewrite > (H x a H3);
- change with ((le x s \land ordered A le (s::l2)) = true).
- apply andb_elim;
- rewrite > H4;
- apply (ordered_injective A le (a::s::l2));
- assumption;
- | intros;
- change with ((le a s \land ordered A le (s::(insert A le x l2))) = true);
- apply andb_elim;
- change in H2 with ((le a s \land ordered A le (s::l2)) = true);
- generalize in match H2;
- apply (andb_elim (le a s));
- elim (le a s);
- [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
- intros;
- apply (H1 s);
- assumption;
- | simplify; intros; assumption
- ]
- ]
- ]
+ intros 5 (A le H l x).
+ 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;
+ elim l'; simplify;
+ [ rewrite > H5;
+ reflexivity
+ | elim (le x s); simplify;
+ [ rewrite > H5;
+ reflexivity
+ | simplify in H4;
+ rewrite > (andb_true_true ? ? H4);
+ reflexivity
+ ]