∀ {α : Type u_1} {p : α → Bool} {as : Array α}
  (motive : (∃ x, (∃ i, ∃ (h : i < as.toList.length), as[i] = x) ∧ p x = true) → Prop)
  (x : ∃ x, (∃ i, ∃ (h : i < as.toList.length), as[i] = x) ∧ p x = true),
  (∀ (i : ℕ) (w : i < as.toList.length) (h : p as[i] = true), motive ⋯) → motive x