Goal:
    A : Type  p : A → bool  a : A  n : nat  pa : is_true (p a)
  ============================
   (is_true (forallb p (repeat a n)))


DEBUG:Going to execute:
induction n

Goals:
    A : Type  p : A → bool  a : A  pa : is_true (p a)
  ============================
   (is_true (forallb p (repeat a 0)))

  
  A : Type
  p : A → bool
  a : A
  n : nat
  pa : is_true (p a)
  IHn : is_true (forallb p (repeat a n))
  ============================
   (is_true (forallb p (repeat a (S n))))


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

Goals:
    A : Type  p : A → bool  a : A  pa : is_true (p a)
  ============================
   (is_true true)

  
  A : Type
  p : A → bool
  a : A
  n : nat
  pa : is_true (p a)
  IHn : is_true (forallb p (repeat a n))
  ============================
   (is_true (p a && forallb p (repeat a n)))


DEBUG:Going to execute:
auto

Goals:
    A : Type  p : A → bool  a : A  pa : is_true (p a)
  ============================
   (is_true true)

  
  A : Type
  p : A → bool
  a : A
  n : nat
  pa : is_true (p a)
  IHn : is_true (forallb p (repeat a n))
  ============================
   (is_true (p a && forallb p (repeat a n)))


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