∀ {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → α'}
  {g : α' → β → γ}, List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun a b => g (f a) b) l₁ l₂