∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : γ → β → γ} {xs : Array α} {init : γ} {stop : ℕ},
  stop = (Array.filterMap f xs).size →
    Array.foldl g init (Array.filterMap f xs) 0 stop =
      Array.foldl
        (fun x y =>
          match f y with
          | some b => g x b
          | none => x)
        init xs