no goals
α : Type u
β : Type u_2
γ : Type u_1
δ : Type ?u.233403
ε : Type ?u.233406
f : α → β → γ
l : List α
l' : List β
n : ℕ
⊢ tail (zipWith f l l') = zipWith f (tail l) (tail l')
simp_rw [← drop_one, zipWith_distrib_drop]