no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.62030
ε : Type ?u.62033
f : α → β
g : α → γ
a : α
l : List α
⊢ zip (map f (a :: l)) (map g (a :: l)) = map (fun a => (f a, g a)) (a :: l)
simp only [map, zip_cons_cons, zip_map']