∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs ys : Array γ} {f : α → β → γ} {as : Array α} {bs : Array β},
  Array.zipWith f as bs = xs ++ ys ↔
    ∃ as₁ as₂ bs₁ bs₂,
      as₁.size = bs₁.size ∧
        as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = Array.zipWith f as₁ bs₁ ∧ ys = Array.zipWith f as₂ bs₂