exact False.elim $ Nat.not_lt_zero i i_lt_zero
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
i : Nat
i_in_bounds : i < a.size
i_lt_zero : i < 0
⊢ p a[i] = true → a[i] ∈ #[].data
no goals