Goal:
  
  A : Type
  P : nat → A → Type
  n : nat
  x : A
  Hnth : nth_error [] n = Some x
  n0 : nat
  ============================
   (P (n0 + n) x)


DEBUG:Going to execute:
destruct n
DEBUG LTAC Evaluated term: HPl

Goals:
  
  A : Type
  P : nat → A → Type
  x : A
  Hnth : nth_error [] 0 = Some x
  n0 : nat
  ============================
   (P (n0 + 0) x)

  
  A : Type
  P : nat → A → Type
  n : nat
  x : A
  Hnth : nth_error [] (S n) = Some x
  n0 : nat
  ============================
   (P (n0 + S n) x)


DEBUG:Going to execute:
discriminate
DEBUG LTAC Evaluated term: n

Goals:
  
  A : Type
  P : nat → A → Type
  x : A
  Hnth : nth_error [] 0 = Some x
  n0 : nat
  ============================
   (P (n0 + 0) x)

  
  A : Type
  P : nat → A → Type
  n : nat
  x : A
  Hnth : nth_error [] (S n) = Some x
  n0 : nat
  ============================
   (P (n0 + S n) x)


DEBUG:Going to execute:
<coq-core.plugins.ltac::discriminate@0>