Goal:
    A : Type  l : list A  n : nat  P : A → bool  d : A
  ============================
   (forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x)


DEBUG:Going to execute:
induction l in n |- *

Goals:
    A : Type  n : nat  P : A → bool  d : A
  ============================
   (forallb P [] → n < #|[]| → ∃ x : A, nth n [] d = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  n : nat
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (forallb P (a :: l) → n < #|a :: l| → ∃ x : A, nth n (a :: l) d = x ∧ P x)


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

Goals:
    A : Type  P : A → bool  d : A
  ============================
   (forallb P [] → 0 < #|[]| → ∃ x : A, nth 0 [] d = x ∧ P x)

    A : Type  n : nat  P : A → bool  d : A
  ============================
   (forallb P [] → S n < #|[]| → ∃ x : A, nth (S n) [] d = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (forallb P (a :: l) → 0 < #|a :: l| → ∃ x : A, nth 0 (a :: l) d = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  n : nat
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (forallb P (a :: l)
    → S n < #|a :: l| → ∃ x : A, nth (S n) (a :: l) d = x ∧ P x)


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

Goals:
    A : Type  P : A → bool  d : A
  ============================
   (true → 0 < 0 → ∃ x : A, d = x ∧ P x)

    A : Type  n : nat  P : A → bool  d : A
  ============================
   (true → S n < 0 → ∃ x : A, d = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (P a && forallb P l → 0 < S #|l| → ∃ x : A, a = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  n : nat
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (P a && forallb P l → S n < S #|l| → ∃ x : A, nth n l d = x ∧ P x)


DEBUG:Going to execute:
auto

Goals:
    A : Type  P : A → bool  d : A
  ============================
   (true → 0 < 0 → ∃ x : A, d = x ∧ P x)

    A : Type  n : nat  P : A → bool  d : A
  ============================
   (true → S n < 0 → ∃ x : A, d = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (P a && forallb P l → 0 < S #|l| → ∃ x : A, a = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  n : nat
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (P a && forallb P l → S n < S #|l| → ∃ x : A, nth n l d = x ∧ P x)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3

Goals:
    A : Type  P : A → bool  d : A
  ============================
   (true → 0 < 0 → ∃ x : A, d = x ∧ P x)

    A : Type  n : nat  P : A → bool  d : A
  ============================
   (true → S n < 0 → ∃ x : A, d = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (P a && forallb P l → 0 < S #|l| → ∃ x : A, a = x ∧ P x)

  
  A : Type
  a : A
  l : list A
  n : nat
  P : A → bool
  d : A
  IHl : ∀ n : nat, forallb P l → n < #|l| → ∃ x : A, nth n l d = x ∧ P x
  ============================
   (P a && forallb P l → S n < S #|l| → ∃ x : A, nth n l d = x ∧ P x)


DEBUG:Going to execute:
try easy