Goal:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT (p i x) (p i x))


DEBUG:Going to execute:
PTRDEBUGTACdestruct (p i x)
DEBUG LTAC Evaluated term: (allbiP (λ (x : nat) (x0 : A), p x x0) p n l)

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT false false)


DEBUG:Going to execute:
PTRDEBUGTACnow constructor
DEBUG LTAC Evaluated term: (p i x)

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT false false)


DEBUG:Going to execute:
PTRDEBUGTACconstructor

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT false false)


DEBUG:Going to execute:
PTRDEBUGTACt; easy

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT false false)


DEBUG:Going to execute:
PTRDEBUGTACt

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (reflectT false false)


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

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (is_true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (false → False)


DEBUG:Going to execute:
PTRDEBUGTACeasy

Goals:
    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (is_true true)

    A : Type  p : nat → A → bool  n : nat  l : list A  i : nat  x : A
  ============================
   (false → False)


DEBUG:Going to execute:
PTRDEBUGTACeasy0 || (solve [ intuition eauto  3 with core terms ])