Ltac inv H := inversion H; clear H; subst.

Ltac cases :=

repeat match goal with

| H: context [ match negb ?x with _ => _ end ] |- _ =>

destruct x; simpl; try solve [inv H; auto]

| H: context [ match ?x with _ => _ end ] |- _ =>

destruct x; try solve [inv H; auto]

| |- context [ match negb ?x with _ => _ end ] =>

destruct x; simpl

| |- context [ match ?x with _ => _ end ] =>

destruct x

end; auto.

Ltac cases_eqn E :=

repeat match goal with

| H: context [ match negb ?x with _ => _ end ] |- _ =>

let E := fresh E in

destruct x eqn: E; simpl; try solve [inv H; auto]

| H: context [ match ?x with _ => _ end ] |- _ =>

let E := fresh E in

destruct x eqn: E; try solve [inv H; auto]

| |- context [ match negb ?x with _ => _ end ] =>

let E := fresh E in

destruct x eqn: E; simpl

| |- context [ match ?x with _ => _ end ] =>

let E := fresh E in

destruct x eqn: E

end; auto.

Tactic Notation "summon" uconstr(ty) "as" ident(id) :=

match goal with H : _ |- _ => pose (id := H : ty); clear id; rename H into id end.

Tactic Notation "take" uconstr(ty) "and" tactic(tac) :=

let new_it := fresh "it"

in try (rename it into new_it);

summon ty as it; tac;

try (rename new_it into it).

Ltac cases :=

repeat match goal with

| H: context [ match negb ?x with _ => _ end ] |- _ =>

destruct x; simpl; try solve [inv H; auto]

| H: context [ match ?x with _ => _ end ] |- _ =>

destruct x; try solve [inv H; auto]

| |- context [ match negb ?x with _ => _ end ] =>

destruct x; simpl

| |- context [ match ?x with _ => _ end ] =>

destruct x

end; auto.

Ltac cases_eqn E :=

repeat match goal with

| H: context [ match negb ?x with _ => _ end ] |- _ =>

let E := fresh E in

destruct x eqn: E; simpl; try solve [inv H; auto]

| H: context [ match ?x with _ => _ end ] |- _ =>

let E := fresh E in

destruct x eqn: E; try solve [inv H; auto]

| |- context [ match negb ?x with _ => _ end ] =>

let E := fresh E in

destruct x eqn: E; simpl

| |- context [ match ?x with _ => _ end ] =>

let E := fresh E in

destruct x eqn: E

end; auto.

Tactic Notation "summon" uconstr(ty) "as" ident(id) :=

match goal with H : _ |- _ => pose (id := H : ty); clear id; rename H into id end.

Tactic Notation "take" uconstr(ty) "and" tactic(tac) :=

let new_it := fresh "it"

in try (rename it into new_it);

summon ty as it; tac;

try (rename new_it into it).