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 |- *; destruct n; simpl; auto