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


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

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

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


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

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

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


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