∀ {α : Type u} (p : α → Bool) (as : Array α) (j : ℕ),
  Array.findFinIdx?.loop✝ p as j =
    if h : j < as.size then if p as[j] = true then some ⟨j, h⟩ else Array.findFinIdx?.loop✝¹ p as (j + 1) else none