∀ {α : Type u} (p : α → Bool) (as : Array α) (i : ℕ) (acc : Array α),
  Array.takeWhile.go✝ p as i acc =
    if h : i < as.size then
      have a := as[i];
      if p a = true then Array.takeWhile.go✝¹ p as (i + 1) (acc.push a) else acc
    else acc