[elim (not_in_list_nil ? ? H)
|elim (in_list_cons_case ? ? ? ? H1)
[rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
[elim (not_in_list_nil ? ? H)
|elim (in_list_cons_case ? ? ? ? H1)
[rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head