- (* XXX destruct H; *)
- change in H' with (Not ((match (x1::tl1) with [nil⇒x1|(cons x1 _) ⇒ x1]) = s));
- rewrite > H in H'; simplify in H'; apply H'; reflexivity;
- | intros; lapply (IH ? H1) as H';
- (* XXX destruct H1 *)
- change in H' with (Not ((match (x1::tl1) with [nil⇒tl1|(cons _ l) ⇒ l]) = l));
- rewrite > H in H'; simplify in H'; apply H'; reflexivity;]]]]
+ destruct H; apply H'; reflexivity;
+ | intros; lapply (IH ? H1) as H'; destruct H;
+ apply H'; reflexivity;]]]]