From Stdlib Require Export String List Bool Lia.

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

Ltac solve_by_inverts n :=
  match goal with | H : ?T |- _ ⇒
    match type of T with Prop ⇒
      solve [
        inversion H;
        match n with S (S (?n')) ⇒
        subst; solve_by_inverts (S n')
      end ]
    end
  end.

Ltac solve_by_invert :=
  solve_by_inverts 1.

Ltac solve_exists_contradiction :=
  match goal with
  | [ Hnot: ¬ (∃ x, ?P x), Hinst: ?P ?val |- _ ] ⇒
      destruct Hnot; ∃ val; exact Hinst
  end.