∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ} {l : List γ} {f : α → β → γ} {l₁ : List α} {l₂ : List β},
  List.zipWith f l₁ l₂ = g :: l ↔ ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = List.zipWith f l₁' l₂'