- [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin
- |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1)
- [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base
- |elim (H H2);elim H3;apply (ex_intro ? ? a);
- apply (ex_intro ? ? a1);apply in_Skip;assumption]]
+ [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
+ |intros 3;
+ elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t);apply in_list_head
+ |elim (H H2);elim H3;apply (ex_intro ? ? a1);
+ apply (ex_intro ? ? a2);apply in_list_cons;assumption]]