Goal:
    A : Type  P : A → bool  n : nat
  ============================
   (on_Some_or_None (λ x : A, P x) (nth_error [] n))


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

Goals:
    A : Type  P : A → bool
  ============================
   (on_Some_or_None (λ x : A, P x) (nth_error [] 0))

    A : Type  P : A → bool  n : nat
  ============================
   (on_Some_or_None (λ x : A, P x) (nth_error [] (S n)))


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

Goals:
    A : Type  P : A → bool
  ============================
   (on_Some_or_None (λ x : A, P x) (nth_error [] 0))

    A : Type  P : A → bool  n : nat
  ============================
   (on_Some_or_None (λ x : A, P x) (nth_error [] (S n)))


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