have h_inductive (idx : Fin a.size) (acc : Array α) (ih : motive idx.1 acc) : motive (idx.1 + 1) (f acc a[idx]) := by
  intro i i_in_bounds i_lt_idx_add_one
  rw [f_def]
  simp only [Fin.getElem_fin]
  intro pai
  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
  . have h := ih i i_in_bounds i_lt_idx pai
    split
    . simp only [Array.push_data, mem_append, mem_singleton]
      exact Or.inl h
    . exact h
  . split
    . simp only [i_eq_idx, Array.push_data, mem_append, mem_singleton, or_true]
    . next pa_idx =>
      simp only [← i_eq_idx] at pa_idx
      exact False.elim $ pa_idx pai
α : 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
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
⊢ 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
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
h_inductive : ∀ (idx : Fin a.size) (acc : Array α), motive (↑idx) acc → motive (↑idx + 1) (f acc a[idx])
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data