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; cbn