rw [zipWithAux_nil_second]
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ (zipWithAux f (cons a x) #[] 0 z).data = List.zipWithTR.go f (cons a x).data #[].data z
case cons.empty
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
z : Array γ
⊢ z.data = List.zipWithTR.go f (cons a x).data #[].data z