∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} {z : γ} {i : ℕ},
  (Array.zipWith f as bs)[i]? = some z ↔ ∃ x y, as[i]? = some x ∧ bs[i]? = some y ∧ f x y = z