∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {n : ℕ} {as : Vector α n} {bs : Vector α_1 n}
  {i : ℕ}, (Vector.zipWith f as bs).take i = Vector.zipWith f (as.take i) (bs.take i)