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


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

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

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


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

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

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


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