elim l
[ simplify; reflexivity;
| simplify;
- generalize in match H1;
- clear H1;
- elim l1;
+ elim l1 in H1 ⊢ %;
[ simplify; reflexivity;
| cut ((le a a1 \land ordered A le (a1::l2)) = true);
[ generalize in match Hcut;
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 a); simplify;