elim l
[ simplify; reflexivity;
| simplify;
- generalize in match H1;
- clear H1;
- elim l1;
+ elim l1 in H1 ⊢ %;
[ simplify; reflexivity;
- | cut ((le t t1 \land ordered A le (t1::l2)) = true);
+ | cut ((le a a1 \land ordered A le (a1::l2)) = true);
[ generalize in match Hcut;
apply andb_elim;
- elim (le t t1);
+ elim (le a a1);
[ simplify;
- fold simplify (ordered ? le (t1::l2));
+ fold simplify (ordered ? le (a1::l2));
intros; assumption;
| simplify;
intros (Habsurd);
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;
+ elim l' in H4 ⊢ %; simplify;
[ rewrite > H5;
reflexivity
- | elim (le x t); simplify;
+ | elim (le x a); simplify;
[ rewrite > H5;
reflexivity
| simplify in H4;
elim l;
[ simplify;
reflexivity;
- | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) t);
+ | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) a);
assumption;
]
qed.
\ No newline at end of file