rw [zipWithAux_nil_first]
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ (zipWithAux f #[] y 0 z).data = List.zipWithTR.go f #[].data y.data z
case empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
y : Array β
z : Array γ
⊢ z.data = List.zipWithTR.go f #[].data y.data z