let motive (idx : Nat) (acc : Array α) : Prop :=
  ∀ i : Nat, ∀ i_in_bounds : i < a.size, i < idx → p (a[i]'i_in_bounds) → (a[i]'i_in_bounds) ∈ acc.data
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
α : 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
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data