conv =>
  lhs
  unfold zipWithAux; dsimp
  rw [dif_pos x.size.zero_lt_succ, dif_pos y.size.zero_lt_succ]
  rw [zipWithAux_cons_cons_succ]
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
b : β
y : Array β
z : Array γ
⊢ zipWithAux f (cons a x) (cons b y) 0 z = zipWithAux f x y 0 (push z (f a b))
no goals