simp [zip, map, map_zip f g xs ys]
α α' β β' : Type
f : α → α'
g : β → β'
x : α
xs : List α
y : β
ys : List β
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip (x :: xs) (y :: ys)) = zip (map f (x :: xs)) (map g (y :: ys))
no goals